To backport a PR, e.g. 1000, to another branch, e.g. `7.0.x`, add a
label `backport 7.0.x` to the PR. This will trigger a workflow which
will create a branch `backport-1000-to-7.0.x` based on the `7.0.x`
branch with a cherry-pick of the PR's merge commit, and create a new PR
for it against the `7.0.x` branch.
It is very simplistic, for instance it doesn't handle cherry-pick
failure gracefully, doesn't validate the state of the PR, doesn't check
if the branch already exists, etc. But we can improve on it later as
needed.
Finally, PRs created by github actions do not themselves trigger further
actions, i.e. the PR isn't checked. You need to close & reopen the PR
for the checks to trigger. There are workarounds for this but they are
either less secure or require more setup.
c85b14391d