From 396a787771909d722e531acf2c11ffec2dd11900 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 09:06:42 -0800 Subject: [PATCH] feat: Reset message log in MainM --- Repl.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Repl.lean b/Repl.lean index 283bcf3..2060061 100644 --- a/Repl.lean +++ b/Repl.lean @@ -79,6 +79,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size set { state with nextId := 0, goalStates := .empty } + Lean.Core.resetMessageLog return .ok { nGoals } stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do let state ← get