Commit 2024-04-07 12:11 38efe796

View on Github →

feat: blacklist compiler definitions in shake (#11981) As reported on Zulip.

Estimated changes

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/Tactic/Eqns.lean

Modified Mathlib/Tactic/Relation/Rfl.lean

Modified Mathlib/Tactic/Widget/SelectInsertParamsClass.lean

Modified Mathlib/Util/CompileInductive.lean

Modified Shake/Main.lean

added def isBlacklisted

Modified scripts/noshake.json