diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index d7df253828e2..642d276bb624 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -571,6 +571,8 @@ where let postNew := (← tacticCacheNew.get).post tacticCache.modify fun _ => { pre := postNew, post := {} } let cmdState ← cmdStateRef.get + -- TODO: should not be done in server mode + let cmdState := Runtime.markPersistent cmdState let mut messages := cmdState.messages if !output.isEmpty then messages := messages.add {