From aa16459c661dda41b84f1835a88a9b4d883e7d27 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 17 Dec 2024 23:03:50 +0100 Subject: [PATCH] fix --- .github/workflows/ci.yml | 1 + src/verso-manual/VersoManual/Docstring.lean | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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