max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: re-enable Elab.async in the server (#6990)

Browse source
This commit is contained in:
Sebastian Ullrich 2025-02-07 17:12:31 +01:00 • committed by GitHub
parent de24063c4b
commit bfe2d28c50
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/FileWorker.lean
View file

@ -353,7 +353,7 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch
let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) fileSetupResult.fileOptions
-- default to async elaboration; see also `Elab.async` docs
--let opts := Elab.async.setIfNotSet opts true
let opts := Elab.async.setIfNotSet opts true
return .ok {
mainModuleName