@coqbot can help with backporting

[x] 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.
[x] 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).

coq / bot