From efa1439ce2639468758144ec9cc8e37471261304 Mon Sep 17 00:00:00 2001 From: Henri Menke Date: Thu, 25 Apr 2019 19:14:46 +1200 Subject: [PATCH] Simpler basename function for extract.lua #640 --- doc/generic/pgf/extract.lua | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/doc/generic/pgf/extract.lua b/doc/generic/pgf/extract.lua index 8b88092ac..c7ea0669d 100644 --- a/doc/generic/pgf/extract.lua +++ b/doc/generic/pgf/extract.lua @@ -89,15 +89,8 @@ local extractor = lpeg.P{"document", -- get the basename and extension of a file local basename = function(file) - local stripper = P{"stripext", - dot = P".", - other = C((1 - V"dot")^0), - stripext = Ct( C(V"dot"^-1) * V"other" * (V"dot" * V"other")^0 ) - } - local matches = lpeg.match(stripper, file) - local ext = table.remove(matches) - local basename = table.concat(matches) - return basename, ext + local basename, ext = string.match(file, "^(.+)%.([^.]+)$") + return basename or "", ext or file end -- Main loop