this patch adds a merge bot. The merge automatically tries to merge a branch from one repository to another. If the merge fails then the bot will open a PR describing the commits that couldn't be merge. Once the conflicts have been resolved and pushed/integrated by a human contributor, then the bot will automatically close the PR.
@edvbld This change can now be integrated. The commit message will be:
Since the source branch of this PR was last updated there has been 1 commit pushed to the
Your changes cannot be rebased automatically without conflicts, so you will need to merge