Skip to content

Commit 4f7258c

Browse files
authored
fix: use loadExts := true in runLinter (#1190)
1 parent ff4cd73 commit 4f7258c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

scripts/runLinter.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ unsafe def runLinterOnModule (update : Bool) (module : Name): IO Unit := do
102102
else
103103
pure #[]
104104
unsafe Lean.enableInitializersExecution
105-
let env ← importModules #[module, lintModule] {} (trustLevel := 1024)
105+
let env ← importModules #[module, lintModule] {} (trustLevel := 1024) (loadExts := true)
106106
let ctx := { fileName := "", fileMap := default }
107107
let state := { env }
108108
Prod.fst <$> (CoreM.toIO · ctx state) do

0 commit comments

Comments
 (0)