diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 41cb632..5e36313 100644 --- 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 index 83a525a..08afb2d 100644 --- 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