diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 83fbfb7c..4e01fc7b 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -480,7 +480,7 @@ def lean : CodeBlockExpanderOf LeanBlockConfig -- Process with empty messages to avoid duplicate output let s ← withTraceNode `Elab.Verso.block.lean (fun _ => pure m!"Elaborating commands") <| - IO.processCommands context { state with pos := startPos } { commandState with messages.unreported := {} } + IO.processCommands context { state with pos := startPos, hasLeading := false } { commandState with messages.unreported := {} } for t in s.commandState.infoState.trees do pushInfoTree t