Skip to content

Commit

Permalink
Update Cli.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser authored Nov 14, 2024
1 parent c9ac6d4 commit 413263e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ImportGraph/Cli.lean
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
| none => none
initSearchPath (← findSysroot)

Lean.enableInitializersExecution
unsafe Lean.enableInitializersExecution
let outFiles ← try unsafe withImportModules (to.map ({module := ·})) {} (trustLevel := 1024) fun env => do
let toModule := ImportGraph.getModule to[0]!
let mut graph := env.importGraph
Expand Down

0 comments on commit 413263e

Please sign in to comment.