Commit 2025-11-20 13:24 9a87f173
View on Github →fix: explicitly enable header linter (#31849)
In files that don't import Mathlib.Init but do import Mathlib.Tactic.Linter.Header, the linter didn't fire currently: the option is only enabled when we define linter.mathlibStandardSet. So in the Mathlib lakefile (but not for downstream projects) we should enable the linter explicitly.
Not sure how we should test this, since it is a lakefile option.
Spotted during review of #31820.