Commit 2024-07-09 09:58 41b65e63
View on Github →fix: silence the set_option linter outside of mathlib (#14558)
This PR makes the set_option linter only emit its warnings in files whose path begins with Mathlib, test, Archive, Counterexamples. Effectively, it should disable the linter on projects that are not mathlib.
Zulip thread