where did the noisy linter go?

Stream: std4

[Kevin Buzzard]

import Std.Tactic.Lint

#check Nat --blue noise

#lint -- All linting checks passed!

Reviewing a mathlib4 PR and it passed the linter checks even though it had a random #check in it. Is this expected? In mathlib3 this would have been flagged by the linter in the PR process.