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") <|

Welcome to the documentation page

-- Temporary comment until the lake issue is resolved -

This was built /-for commit {s!"{← getProjectCommit} "}-/ using Lean 4 at commit {Lean.githash}

+ -- for commit {s!"{← getProjectCommit} "} +

This was built using Lean 4 at commit {Lean.githash}

end Output