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