From 0ecbcfdcc3785c155b8f394c655f48f4f7ed0e65 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 15 Aug 2024 17:41:42 +0200
Subject: [PATCH] chore: remove stray `markPersistent` (#5056)

It is conditionally applied a few lines below
---
 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 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