fix: message duplication in log (#7)

leanprover · Jul 19, 2024 · 6c92ccc · 6c92ccc
1 parent 3f7d192
commit 6c92ccc
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Manual/Meta.lean b/Manual/Meta.lean
@@ -185,6 +185,7 @@ def leanInline : RoleExpander
       let (newMsgs, tree) ← withInfoTreeContext (mkInfoTree := mkInfoTree `leanInline (← getRef)) do
         let initMsgs ← Core.getMessageLog
         try
+          Core.resetMessageLog
           discard <| Elab.Term.elabTerm stx none
           Core.getMessageLog
         finally