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