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

Estimated changes