Closed juliaogris closed 3 years ago
We should probably squash merge these as it gives the opportunity to reword the title to add the emoji and PR number. It means we could also add the diff stat at the end and the Pull-Request link. Whereas a FF merge will lose any PR information.
I will have to figure out how to do squash merges from the CLI. It may involve the github API, and at that point, maybe it makes sense to use our own hub
tool that does it for us (assuming hub
does not)
Done in db16598bc85d1b8f3a59e8c0d3778590401b972a - no diff stat was added as that is not needed for a single commit, but the Pull-Request
trailer is added. This was initially done with hub api
but since moving to gh
, gh pr merge --squash
does it more simply.
[Squash merging was originally done in d4ee6c5fbd67e6fad391f33cfabcb7a836c20a31 - the above mentioned PR just uses it automatically for single PR commits]
In order to avoid commit histories like this:
consider using FF merges for single commit PRs.