Mathlib Changelog
v4
Changelog
About
Github
Def
prTitle
Modification history
2025-11-19 14:54
Mathlib/Tactic/Linter/ValidatePRTitle.lean
feat: check for PR titles which do not start with "feat" etc. (#29512) …
Added
prTitle
View on Github →