Skip to content

Commit

Permalink
feat: disable old cmdline driver
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed May 27, 2024
1 parent 6677767 commit ff00003
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Elab/Frontend.lean
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ def runFrontend
: IO (Environment × Bool) := do
let startTime := (← IO.monoNanosNow).toFloat / 1000000000
let inputCtx := Parser.mkInputContext input fileName
if true then
if false then
-- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-- overhead of passing the environment between snapshots until we actually make good use of it
-- outside the server
Expand Down

0 comments on commit ff00003

Please sign in to comment.