We now atomically push the result of integrating to the main branch and the PR branch. This should hopefully avoid the problem from #196. By pushing atomically, we hope that GitHub will handle both pushes at the same time and only check for the merging/closing after both have been handled.
We now atomically push the result of integrating to the main branch and the PR branch. This should hopefully avoid the problem from #196. By pushing atomically, we hope that GitHub will handle both pushes at the same time and only check for the merging/closing after both have been handled.