The workflow for merging PRs in the Github interface and triggering backports, is very straightforward, but it would be useful to document it for core developers unfamiliar with it (as otherwise it's easy to think "have I missed something?")