[jbosstools-dev] Merge PRs from GitHub UI

[Max Rydahl Andersen]

> 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