[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. 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