From 6dcf6310a36a9f1505e63e82ad121b6f8768d509 Mon Sep 17 00:00:00 2001
From: Simon Michael <simon@joyful.com>
Date: Mon, 6 Jan 2020 07:07:19 -0800
Subject: [PATCH] ;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]
---
 Shake.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Shake.hs b/Shake.hs
index c6dbf5a36..1599efe40 100755
--- a/Shake.hs
+++ b/Shake.hs
@@ -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: