Commit 2025-04-14 11:08 a6c0d685
View on Github →chore: remove now-superfluous disabling of the header linter (#24028) PR https://github.com/leanprover-community/mathlib4/pull/24027 removes the need to disable the header linter before module deprecations.