Sqash commits

[Y-Less]

This is just a note, as there isn't really a good way to discuss things on Github. People seem to talk about how squash commits are a good way to merge requests. The feature branch keeps all the individual commits, while the main branch gets a single commit with a complete feature and a clean history. Github has even added a "squash" option to their web-based pull request merge. I tried this for the first time on three PRs yesterday: #441 #447 and #372.

I won't be doing that again. There seems to be absolutely no mention of the original authors (@Daniel-Cortez and @YashasSamaga) in the commits, nor any links (except in the text of the commit message) to the original commits. As a result it just looks like I commited a load of stuff and closed some pull requests, whereas what actually happened was I tried to merge. All those git usage guides that advocate squash? Ignore them!

Sorry @Daniel-Cortez and @YashasSamaga.

[Y-Less]

I did re-merge them, but I don't know if that is a bit silly as well, to end up with several merge commits making no changes.

[Daniel-Cortez]

@Y-Less I think it would be valid to add a "(merged)" prefix to the titles of those PRs, so the others could easily see that those PRs were actually merged and not rejected (could be useful for a job interview, for example).

And if you're going to do this, can you please also add that prefix to #353? It seems it was "merged" in the same manner. Thank you in advance.

[Southclaws]

Why not simply merge using the GitHub UI?

[Y-Less]

Because I wanted to build and test them all together first.

[Southclaws]

Then you can merge locally and test, then perform the final merge on GitHub.

Or alternatively, if others wish to test after you merge, you can merge to another temporary branch to stage all the changes together, then merge the original into the dev branch via GitHub and delete the staging branch.

[Y-Less]

Yeah, probably.