Commit 2025-04-14 09:20 7e897609
View on Github →fix(deprecated module): automatically disable the header linter (#24027)
This PR makes the header linter silent if the first non-import command of a file is deprecated_module.
[Zulip#mathlib4 > `Deprecated` folder @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Deprecated.60.20folder/near/511986519)