[hibernate-dev] Github offering new options about how the big "green button" to merge Pull Requests

Github now offers an option to not create the "merge commit" when you want to merge a PR from the web ui. It comes at a significant cost though: it will merge the PR but squash all commits in one. While initially thinking that doesn't help us at all, at second thought: we really want any non-trivial code change to be checked out locally, run the testsuite, and only then push. But let's say there's a trivial PR fixing some typos in documentation! You look at it, looks good and then you really just want to say "go ahead" and get back to more important matters. Besides, we have Jenkins carefully testing these too and it will grey out the button if the build fails, so there's some kind of last defence in case you didn't notice that the "docs typo" PR actually sneaks in some real problem. So I'd say we could enable this option with the "squashing" ? We would still refrain from using the green button for most patches, but it could save some "boring process" minutes for those simpler patches. I've enabled this option for Hibernate Search. We can seek team consensus before actually using it (you're not supposed to use the "green button" at all currently), I might at least have it default to the less annoying option: if you do use it by mistake, it will squash it all. The open question remains if we're ok to use it regularly for trivial PRs, and if you want this switched on all Hibernate repositories. Thanks, Sanne