diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index e4bcb714f146f..41832c0f4570b 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -65,12 +65,9 @@ This means that CI will eventually fail on `#`-commands, but does not stop it fr However, in order to avoid local clutter, when `warningAsError` is `false`, the linter logs a warning only for the `#`-commands that do not already emit a message. -/ def hashCommandLinter : Linter where run := withSetOptionIn' fun stx => do - let mod := (← getMainModule).components if Linter.getLinterValue linter.hashCommand (← getOptions) && - ((← get).messages.reportedPlusUnreported.isEmpty || warningAsError.get (← getOptions)) && - -- we check that the module is either not in `test` or, is `test.HashCommandLinter` - (mod.getD 0 default != `test || (mod == [`test, `HashCommandLinter])) - then + ((← get).messages.reportedPlusUnreported.isEmpty || warningAsError.get (← getOptions)) + then if let some sa := stx.getHead? then let a := sa.getAtomVal if (a.get ⟨0⟩ == '#' && ! allowed_commands.contains a) then