Skip to content

Commit f3c759d

Browse files
committed
fix overwrite_index.lean
1 parent f7c78bf commit f3c759d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

docbuild/scripts/overwrite_index.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@ unsafe def runWithImports {α : Type} (actionToRun : CoreM α) : IO α := do
100100
let currentCtx := { fileName := "", fileMap := default }
101101
Lean.enableInitializersExecution
102102

103-
Lean.withImportModules modulesToImport {} 0 fun env => do
103+
Lean.withImportModules modulesToImport {} fun env => do
104104
let (result, _newState) ← Core.CoreM.toIO actionToRun currentCtx { env := env }
105105
return result
106106

0 commit comments

Comments
 (0)