From 7b7781d20e271923257cdde49700b6344a8fa917 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 15 Aug 2024 16:23:26 +0200 Subject: [PATCH] chore: remove stray `markPersistent` --- src/Lean/Language/Lean.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index b212eba55d49..3a2b936aa580 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