jltaylor-us
commented
1 year ago In this specific case, I don't think there's anything to be gained by keeping the commit history. In other circumstances (when editing code instead of docs), I'll generally try to make each commit a logical self-contained, coherent unit (in which case the commit history might be useful). My general observations from other projects are that unless everyone is committed (no pun intended) to making their branch histories "useful" that keeping those histories is pointless. (In other words, squashing is probably a good default... although it occurs to me that part of the reason for that is that I don't think the GitHub UI has any option that's the equivalent of using the --first-parent flag to git log.)
You might also want to wait a bit to see if the other Chez maintainers have any feedback on the PR, since I pinged everyone via email. (Although I don't think there's anything stopping them from adding comments after it's already merged?)
mflatt
Thanks!
Do you have an opinion on merges and Git history? I would normally squash a set of changes like this to a single commit, because I find that more useful when looking at Git history. But keeping the history and merge commits is also ok with me.