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

[Sanne Grinovero]

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