max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fold sub-chapters by default

Browse source
This commit is contained in:
Sebastian Ullrich 2022-04-20 18:46:30 +02:00
parent b6446902c2
commit 5f6bbe59ef
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/book.toml
View file

@ -13,5 +13,9 @@ git-repository-url = "https://github.com/leanprover/lean4"
additional-css = ["alectryon.css", "pygments.css"]
additional-js = ["alectryon.js"]
[output.html.fold]
enable = true
level = 0
[output.html.playground.boring-prefixes]
lean = "# "