r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: save the expansion state of the tree again

main
Henrik Böving 2022-12-13 20:00:07 +01:00
parent 8fd0520dc0
commit f221bbdcff
2 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
DocGen4/Output/Navbar.lean
View File

@ -61,6 +61,7 @@ def navbar : BaseHtmlM Html := do
<head> <head>
[←baseHtmlHeadDeclarations] [←baseHtmlHeadDeclarations]
<script type="module" src={s!"{←getRoot}nav.js"}></script>
<base target="_parent" /> <base target="_parent" />
</head> </head>

1
DocGen4/Output/Template.lean
View File

@ -32,7 +32,6 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
<script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script> <script>{s!"const SITE_ROOT={String.quote (←getRoot)};"}</script>
[moduleConstant] [moduleConstant]
<script type="module" src={s!"{←getRoot}nav.js"}></script>
<script type="module" src={s!"{←getRoot}search.js"}></script> <script type="module" src={s!"{←getRoot}search.js"}></script>
<script type="module" src={s!"{←getRoot}how-about.js"}></script> <script type="module" src={s!"{←getRoot}how-about.js"}></script>
<script type="module" src={s!"{←getRoot}instances.js"}></script> <script type="module" src={s!"{←getRoot}instances.js"}></script>