diff --git a/Mathlib/Tactic/Linter/Lint.lean b/Mathlib/Tactic/Linter/Lint.lean
index df3932bb0ac937..d2ca3a477dd73b 100644
--- a/Mathlib/Tactic/Linter/Lint.lean
+++ b/Mathlib/Tactic/Linter/Lint.lean
@@ -175,6 +175,9 @@ def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.endOf o
 def endOfLinter : Linter where run := withSetOptionIn fun stx ↦ do
     -- Only run this linter at the end of a module.
     unless stx.isOfKind ``Lean.Parser.Command.eoi do return
+    -- TODO: once mathlib's Lean version includes leanprover/lean4#4741, make this configurable
+    unless #[`Mathlib, `test, `Archive, `Counterexamples].contains (← getMainModule).getRoot do
+      return
     if getLinterHash (← getOptions) && !(← MonadState.get).messages.hasErrors then
       let sc ← getScopes
       -- The last scope is always the "base scope", corresponding to no active `section`s or
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index ba6d2c164fdf8b..fbceb4a721f865 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -58,6 +58,7 @@ def setOptionLinter : Linter where run := withSetOptionIn fun stx => do
       return
     if (← MonadState.get).messages.hasErrors then
       return
+    -- TODO: once mathlib's Lean version includes leanprover/lean4#4741, make this configurable
     unless #[`Mathlib, `test, `Archive, `Counterexamples].contains (← getMainModule).getRoot do
       return
     if let some head := stx.find? is_set_option then