;doc: strip html comments, preserved by latest pandoc (?)

Not sure when the --strip-comments option was added, but we seem
to need it now.

[ci skip]
This commit is contained in:
Simon Michael 2020-01-06 07:07:19 -08:00
parent 3bf6ef9a8b
commit 6dcf6310a3

View File

@ -104,7 +104,7 @@ usage = unlines
-- groff = "groff -c" ++ " -Wall" -- see "groff" below
makeinfo = "makeinfo" ++ " --no-warn" -- silence makeinfo warnings - comment out to see them
pandoc = "pandoc"
pandoc = "pandoc --strip-comments"
-- Must support both BSD sed and GNU sed. Tips:
-- BSD: