diff options
| -rwxr-xr-x | luaotfload-tool.lua | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/luaotfload-tool.lua b/luaotfload-tool.lua index 4afd9d1..5028515 100755 --- a/luaotfload-tool.lua +++ b/luaotfload-tool.lua @@ -1338,16 +1338,22 @@ do if asked.files == true then errcnt = verify_files (errcnt, info) + asked.files = nil end if asked.permissions == true then errcnt = check_permissions (errcnt) + asked.permissions = nil end if asked.repository == true then --errcnt = check_upstream (info.notes.revision) check_upstream (info.notes.revision) + asked.repository = nil end - + local rest = next (asked) + if rest ~= nil then --> something unknown + out ("Unknown diagnostic “%s”.", rest) + end if errcnt == 0 then --> success out ("Everything appears to be in order, \z you may sleep well.") |