From 628ef2878e994abed48185e4d94784c8403bf4c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 16 Mar 2023 20:24:44 +0100
Subject: [PATCH] fix: properly comment out for the workaround

---
 DocGen4/Output/Index.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index 0bc21d5..afa4eb5 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -17,7 +17,8 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
       <a id="top"></a>
       <h1> Welcome to the documentation page </h1>
       -- Temporary comment until the lake issue is resolved
-      <p>This was built /-for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a>-/ using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
+      -- for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a>
+      <p>This was built using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
     </main>
 
 end Output