Re: [jbosstools-dev] Merge PRs from GitHub UI
Hi,
In April, GitHub introduced squashed merging[1] to their web UI. It's
now
OK to use the big green "merge" button for PRs in Github for
openshift, as
commits in a PR will be squashed commits and put at the tip of the
branch. It's
not as nice as having rebase support but that's better than before.
Still not a fan of the green button - should only be used for most
trivial things.
I would say if we have PR jobs setup that verifies the new tests passes
the git green button would be great to use with this new setup :)
But sure, its great github at least allow some smaller fixes being
merged in a simpler way.
It works beautifully for >90% of the PRs (from my very
unscientific
estimations). However there are cases where you shouldn't use that
button:
- when there are merge conflicts (but the UI won't let you anyway)
- if you really intend on keeping distinct commits in the PR. This is
especially important when the PR contains commits from different
authors.
*Everything* will be squashed, only one author will remain.
But there are 2 added benefits of using the merge button: it marks the
PR
as merged, not closed (also shown in JIRA), and it adds the PR # in
the
commit message, so it's easy to link back to the original PR.
So I went ahead and disabled merge commits for all (I think)
jbosstools
repositories on GitHub, to make it easier to merge PRs (and prevent
accidental merge commits). If anyone wants me to undo that change for
specific repos, please lemme know.
I have a feeling this would collide with how most automatic merge PR
request builders would work - but we can enable it again for such
projects when we have them.
/max
http://about.me/maxandersen