From f4ef29b80039c2f989793283c878be7fe56efe7d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Dec 2020 17:46:46 +0100 Subject: [PATCH] chore: remove obsolete workaround --- src/Lean/Server/FileWorker.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index a4931bd969..b2da377837 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -127,9 +127,7 @@ section ServerM def compileDocument (m : DocumentMeta) : ServerM Unit := do let headerSnap@⟨_, _, _, SnapshotData.headerData env msgLog opts⟩ ← Snapshots.compileHeader m.text.source | throwServerError "Internal server error: invalid header snapshot" - -- TODO(WN): Remove the hardcoded option once the server is linked against stage0 - let opts' := opts.setBool `interpreter.prefer_native false - let headerSnap' := { headerSnap with data := SnapshotData.headerData env msgLog opts' } + let headerSnap' := { headerSnap with data := SnapshotData.headerData env msgLog opts } let cmdSnaps ← unfoldCmdSnaps m headerSnap (←read).docRef.set ⟨m, headerSnap, cmdSnaps⟩ @@ -310,4 +308,4 @@ def workerMain : IO UInt32 := do e.putStrLn (toString err) return 1 -end Lean.Server.FileWorker \ No newline at end of file +end Lean.Server.FileWorker