remove obsolete Lean.enableInitializersExecution

leanprover-community · Dec 10, 2024 · f80066c · f80066c
1 parent 123ff1a
commit f80066c
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/check-yaml.lean b/scripts/check-yaml.lean
@@ -40,7 +40,6 @@ def processDb (decls : ConstMap) : String → IO Bool
     return false
 
 unsafe def main : IO Unit := do
-  Lean.enableInitializersExecution
   CoreM.withImportModules #[`Mathlib, `Archive]
       (searchPath := compile_time_search_path%) (trustLevel := 1024) do
     let decls := (← getEnv).constants