From fe73a10591e62ff0a6bc14de527c0c7d76caffc6 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 15 Aug 2024 16:59:20 +0200 Subject: [PATCH] fix(lint-style): ignore Batteries module --- scripts/lint-style.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 2947d7b35daf0b..5c7ab0d34064f8 100644 --- 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.