@coqbot can help with backporting

[Zimmi48]

• When a PR is merged, if the milestone description contained "coqbot: backport to BRANCH (request inclusion column: URL1 / backported column: URL2)", and the PR was not targeting BRANCH already, then put the PR in the project column URL1.
• When new commits are pushed, if their message is "Backport #PRNUM..." or "Merge #PRNUM..." and the description of the milestone for the corresponding PR contained the above text, then put / move these PRs to the project column URL2.
• At the time of putting a PR in the request inclusion column, backport this PR to the backport branch of @coqbot's fork of the Coq repository (if it can be done without solving conflicts) and open a PR for this branch if the branch didn't exist (and delete the branch whenever the corresponding PR is merged).

[Zimmi48]

@coqbot currently pushes what it can backport to a staging branch on Coq's GitLab repository. Related: #18