Commit: df29e24d3846df727ed1cfd2e717010a73701a5e
Parent: 451b80abb5c809584b4133c693530874d5d3c9dc
Author: Michael Forney
Date: Thu, 8 Feb 2024 20:18:02 -0700
man: add '.gz' extension when needed
Diffstat:
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/ninja.lua b/ninja.lua
@@ -496,11 +496,13 @@ function man(srcs, section)
local ext = base:match('%.([^.]*)$')
if ext then base = base:sub(1, -(#ext + 2)) end
if section then ext = section end
+ local path = 'share/man/man'..ext..'/'..base..'.'..ext
if config.gzman ~= false then
build('gzip', out, src)
src = out
+ path = path..'.gz'
end
- file('share/man/man'..ext..'/'..base..'.'..ext, '644', src)
+ file(path, '644', src)
end
end