From f221bbdcffe6a17bb310f0e9ee10767812b03e13 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 13 Dec 2022 20:00:07 +0100 Subject: [PATCH] fix: save the expansion state of the tree again --- DocGen4/Output/Navbar.lean | 1 + DocGen4/Output/Template.lean | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index fb5fbe3..9842bba 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -61,6 +61,7 @@ def navbar : BaseHtmlM Html := do [←baseHtmlHeadDeclarations] + diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 432d070..ed00bd9 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -32,7 +32,6 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d [moduleConstant] -