Just used the "Merge Pull Request" button now that we have GitBox and that felt good.
Now that we have push access to github, I believe we want some changes to our git flow. Here's some thoughts: 1. Avoid manual merges for most things and prefer the "Merge PR" button in GitHub 2. Issue PRs to each branch that will be updated 3. Use the "Merge PR" button in reverse version order (as we should be doing now with manual merges - merge master first, then tp33 and then tp32) 4. I suppose that for external PRs we could ask the submitter to issue multiple PRs depending on the base branch they are targeting, but that might create some extra friction for new contributors. Maybe we committers should just create those PRs for them in those cases (unless they are conflicted badly then perhaps the submitter should go back and deal with that). 5. CTRs will still need manual merging so I guess that doesn't go away. Any other ideas?
