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

doc: add # prefix to hide lines in lean code blocks

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-30 16:00:20 +01:00
parent ac0d0ab32d
commit 2129798376
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
doc/book.toml
View file

@ -10,3 +10,6 @@ build-dir = "out"
[output.html]
git-repository-url = "https://github.com/leanprover/lean4"
[output.html.playground.boring-prefixes]
lean = "# "