diff --git a/scripts/runLinter.lean b/scripts/runLinter.lean index 4f18be6b50..2cc11a05b9 100644 --- a/scripts/runLinter.lean +++ b/scripts/runLinter.lean @@ -52,7 +52,7 @@ unsafe def main (args : List String) : IO Unit := do readJsonFile NoLints nolintsFile else pure #[] - withImportModules #[{module}] {} (trustLevel := 1024) fun env => + withImportModules #[{module}, { module := `Batteries.Tactic.Lint }] {} (trustLevel := 1024) fun env => let ctx := { fileName := "", fileMap := default } let state := { env } Prod.fst <$> (CoreM.toIO ยท ctx state) do