diff --git a/doc/book.toml b/doc/book.toml index 024831634c..1c8634d5b7 100644 --- a/doc/book.toml +++ b/doc/book.toml @@ -10,3 +10,6 @@ build-dir = "out" [output.html] git-repository-url = "https://github.com/leanprover/lean4" + +[output.html.playground.boring-prefixes] +lean = "# "