Skip to content

Commit

Permalink
change default to sync, minus persistent exts
Browse files Browse the repository at this point in the history
  • Loading branch information
Kha committed Jan 31, 2025
1 parent 7c59d7d commit c2a80b2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Environment.lean
Original file line number Diff line number Diff line change
Expand Up @@ -869,7 +869,7 @@ end EnvExtension
Note that by default, extension state is *not* stored in .olean files and will not propagate across `import`s.
For that, you need to register a persistent environment extension. -/
def registerEnvExtension {σ : Type} (mkInitial : IO σ)
(asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO (EnvExtension σ) := do
(asyncMode : EnvExtension.AsyncMode := .sync) : IO (EnvExtension σ) := do
unless (← initializing) do
throw (IO.userError "failed to register environment, extensions can only be registered during initialization")
let exts ← EnvExtension.envExtensionsRef.get
Expand Down

0 comments on commit c2a80b2

Please sign in to comment.