Skip to content

Commit 0f0d2ce

Browse files
committed
chore: add workaround for regression in latest nightly
1 parent a6000da commit 0f0d2ce

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Manual/Meta/ErrorExplanation.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -435,7 +435,7 @@ def closeEnclosingSection : PartElabM Unit := do
435435
throwError m!"Failed to close the last-opened explanation part"
436436

437437
/-- Adds explanation blocks until the "Examples" header is reached. -/
438-
def addNonExampleBlocks := do
438+
def addNonExampleBlocks : ExplanElabM Unit := do
439439
repeat
440440
let some block ← ExplanElabM.nextBlock?
441441
| return

0 commit comments

Comments
 (0)