diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index b212eba55d..3a2b936aa5 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -597,7 +597,7 @@ where -- definitely resolve eventually snap.new.resolve <| .ofTyped { diagnostics := .empty : SnapshotLeaf } - let mut infoTree := Runtime.markPersistent cmdState.infoState.trees[0]! + let mut infoTree := cmdState.infoState.trees[0]! let cmdline := internal.cmdlineSnapshots.get scope.opts && !Parser.isTerminalCommand stx if cmdline then infoTree := Runtime.markPersistent infoTree