also import Batteries.Tactic.Lint

leanprover-community · Aug 22, 2024 · b187647 · b187647
1 parent d747f07
commit b187647
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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