Hi all,
Github just released a new "rebase merging" feature, which makes merging PRs as
clean as doing the merge by hand. See
https://github.com/blog/2243-rebase-and-merge-pull-requests.
I'd like to propose that we always "rebase merge" PRs. There may be occasions
where we would not do this, but I expect they are rare.
Here are the merge button options that can be toggled:
* Allow merge commits
Add all commits from the head branch to the base branch with a merge
commit.
* Allow squash merging
Combine all commits from the head branch into a single commit in the
base branch.
* Allow rebase merging
Add all commits from the head branch onto the base branch individually.
Shall we also ask INFRA to disable any of these merge options?
J
