From d5915fcb13e4e12e384686e849e315ee833a3a8b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 11:25:10 +0100 Subject: [PATCH] Revert "feat: Fix siteRoot in JS" This reverts commit dcd57e8c5f1bbe34ec5d1b13ee25bbb44dd21c49. --- DocGen4/Output/Template.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 0e28fc6..5d82257 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -45,7 +45,7 @@ def baseHtml (title : String) (site : Html) : HtmlM Html := do -- Lean in JS in HTML in Lean...very meta -- TODO Add more js stuff