Update Load.lean

leanprover · Dec 9, 2024 · 5ef12ec · 5ef12ec
1 parent fae3926
commit 5ef12ec
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
@@ -11,7 +11,7 @@ open Lean System IO
 
 def envOfImports (imports : Array Name) : IO Environment := do
   -- needed for modules which use syntax registered with `initialize add_parser_alias ..`
-  Lean.enableInitializersExecution
+  unsafe Lean.enableInitializersExecution
   importModules (imports.map (Import.mk · false)) Options.empty (leakEnv := true)
 
 def loadInit (imports : Array Name) : IO Hierarchy := do