From 2129798376421b3e66751182ecc36d23050ab9de Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 30 Oct 2020 16:00:20 +0100
Subject: [PATCH] doc: add `# ` prefix to hide lines in `lean` code blocks

---
 doc/book.toml | 3 +++
 1 file changed, 3 insertions(+)

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 = "# "