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.
