Commit 2024-07-15 20:56 fd21dab2

View on Github →

chore: rename endOf linter to missingEnd (#14758) Per zulip discussion.

Estimated changes

Modified Mathlib/Tactic/Linter/Lint.lean

deleted def Mathlib.Linter.EndOf.endOfLinter

deleted def Mathlib.Linter.EndOf.getLinterHash

added def Mathlib.Linter.MissingEnd.getLinterHash

added def Mathlib.Linter.MissingEnd.missingEndLinter