From 076da7dd18f9d0c9149765b7d04573f404c1ca66 Mon Sep 17 00:00:00 2001
From: Simon Michael <simon@joyful.com>
Date: Sun, 21 Mar 2021 09:01:33 -0700
Subject: [PATCH] ;shake webmanuals: update toc/versions placeholders

---
 Shake.hs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Shake.hs b/Shake.hs
index d9f62a602..ba3dee342 100755
--- a/Shake.hs
+++ b/Shake.hs
@@ -498,8 +498,10 @@ main = do
         -- But cmd Shell doesn't handle arguments containing spaces properly.
         liftIO $ writeFile out $ unlines [
            "<!-- " ++ "Generated by \"Shake webmanuals\" from " ++ unwords deps ++ " -->"
-          ,""
-          , "<!-- toc -->"
+          ,"<div class=\"docversions\"></div>"
+          ,"<div class=\"pagetoc\">"
+          ,"<!-- toc -->"
+          ,"</div>"
           ,""
           ,"# " ++ heading
           ,""