diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index ab75e7a9f5..659dede5ba 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -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