From dcd57e8c5f1bbe34ec5d1b13ee25bbb44dd21c49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 09:32:21 +0100 Subject: [PATCH] feat: Fix siteRoot in JS --- 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 5d82257..0e28fc6 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