Fix typos.

[waywardmonkeys]

No description provided.

[waywardmonkeys]

Updated with a couple of additional typo fixes.

[rptb1]

I have checked that all these changes are in comments or design document text. There is one change to a tag, but that tag is not referenced (according to a comprehensive grep). So I do not think it's possible for these changes to introduce any defects.

[rptb1]

I'm going to use this PR to experiment with using GitHub's "Merge pull request" button, with the "Create a merge commit" option, which might be suitable for replacing step 5 of proc.merge.pull-request in some circumstances.

[rptb1]

A couple of comments on adopting the use of the merge button.

It does offer a way to edit the merge commit comment, like this:

If we merge in this way from an outside fork (as in the case of this pull request) we don't get a local named branch, and when the outside person deletes their branch, we've lost information that keeps multiple changes together. Therefore we should not use the button when there are multiple changes in a PR.

[waywardmonkeys]

If you do a merge commit, that's preserving the history. Deleting the origin branch has no bearing on what is stored within the repository.

[rptb1]

If you do a merge commit, that's preserving the history. Deleting the origin branch has no bearing on what is stored within the repository.

Kinda sorta, as long as the merge has some sort of relationship to its purpose. Which is why we must be careful to preserve the reference to the pull request, its discussion, reviews, the issues and events that caused it, and the work done, which includes the branches created, when they were made, where, from what, and why, by whom, etc.

There are multiple threads like https://stackoverflow.com/questions/1527234/finding-a-branch-point-with-git with people trying to figure out what's happened in the tangled mess of Git history, because Git fails to record intention at all well.

And don't get me started on squashing and forced pushes. We have emails in the archive that refer to Git hashes that are just gone from the universe, and so we don't know what they are talking about.

One of the things I'm concerned with is that the MPS has a multi-decade history across three version control systems. Maybe there won't be a fourth, but I'm not betting against it by discarding information in favour of Git's impoverished recording of intention.