This is a new step in my crusade against the braindead fad of starting
PR titles with a word that is completely redundant with github labels,
thus wasting prime first-line real-estate for something that isn't
necessary.
I noticed that every single one of these PRs are low-quality AI-slop, so
I think there is a strong case to be made for these PRs to be
auto-closed. A message is added before closing the PR, redirecting to
our contribution guidelines, so I expect quality first-time contributors
to read them and reopen the PR. In the case of spam PRs, the author is
unlikely to revisit a given PR, and so auto-closing might have a
positive impact. That's an experiment worth trying, imo.
A new pointless fad appeared recently where people just create a fairly
low information tag at the beginning of their github PR titles.
Something like `feat` or other keywords.
This seems to originate from the angular community and to be used for
automation scripts over there. We do not use any of those scripts and if
we did we would be using the github labels, which offer strictly
equivalent functionalities without wasting useful PR title space.
In order for these keywords to fail the validation, I am adding a check
that these directories listed indeed exist in the repository.
Full disclosure: this has been generated by AI. The goal is to have a
quick check that the PR format is correct, before we merge it. This is
to avoid the periodical case when someone forgets to add a milestone or
check the title matches our preferred format.
