[jbosstools-dev] Merge PRs from GitHub UI

[Fred Bricon]

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.

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.

Fred

[1] https://github.com/blog/2141-squash-your-commits
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.jboss.org/pipermail/jbosstools-dev/attachments/20160509/ee62df11/attachment.html