fix

leanprover · Dec 18, 2024 · 573d97f · 573d97f
1 parent 2ad9217
commit 573d97f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -94,6 +94,7 @@ jobs:
             sourceserifpro
             fvextra
             upquote
+            lineno
 
       - name: Check `tlmgr` version
         run: tlmgr --version

diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
@@ -921,7 +921,7 @@ def docstring : BlockRoleExpander
       let sig := Lean.Widget.tagCodeInfos ctx infos tt
       let signature ← some <$> renderTagged none sig ⟨{}, false⟩
       let extras ← getExtras name declType
-      pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$blockStx,*, $extras,*])]
+      pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$(blockStx ++ extras),*])]
     | _ => throwError "Expected exactly one positional argument that is a name"
   | _, more => throwErrorAt more[0]! "Unexpected block argument"
 where
-Original file line number
+Diff line change
@@ Expand Up / @@ -94,6 +94,7 @@ jobs: @@
                 sourceserifpro
                 fvextra
                 upquote
+                lineno
           - name: Check `tlmgr` version
             run: tlmgr --version
@@ Expand Down @@