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