fix: make docstring CSS fit Lean graphical identity

leanprover · Sep 6, 2024 · 57e9c52 · 57e9c52
1 parent c239b63
commit 57e9c52
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/Manual/Meta/Syntax.lean b/Manual/Meta/Syntax.lean
@@ -349,7 +349,9 @@ def syntax.descr : BlockDescr where
       pure {{
         <div class="namedocs" {{attrs}}>
           <span class="label">"syntax"</span>
-          {{← content.mapM goB}}
+          <div class="text">
+            {{← content.mapM goB}}
+          </div>
         </div>
       }}
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "211324b7781e85202bf885f6accac506ca9de5e9",
+   "rev": "099f82f9faa3f550f242df55dbacba160bf86fa4",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",