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 checkTitleLabelsView on Github →