fix(lint-style): ignore Batteries module

leanprover-community · Aug 15, 2024 · fe73a10 · fe73a10
1 parent b2e9f4c
commit fe73a10
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean
@@ -26,6 +26,8 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let mut allModules := #[]
   for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do
     allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import "))
+  -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually
+  allModules := allModules.erase "Batteries"
   let numberErrorFiles ← lintModules allModules mode (args.hasFlag "fix")
   -- Make sure to return an exit code of at most 125, so this return value can be used further
   -- in shell scripts.