chore: fix typos, remove extra spaces #121
Conversation
| @@ -108,7 +108,7 @@ intro n k | |||
| ``` | |||
| :::: | |||
|
|
|||
| The {tactic}`case` and {tactic}`case'` tactics can be used to select a new main goal using the desired goal's name. | |||
| The {tactic}`case` and {tactic}`case'` tactics can be used to select a new main goal using the desired goal's name. | |||
There was a problem hiding this comment.
I can't even see the change here in the GH interface. What changed?
There was a problem hiding this comment.
I think you have to scroll to the right: desired goal (two spaces) is changed to desired goal (one space).
There was a problem hiding this comment.
Yep, now I see it :)
|
Thanks! This looks like it was automatically generated - in particular, it's "correcting" a US spelling to a UK spelling in a vendored JS dependency. What script did you use? Can you please remove the changes to the vendored JS dependencies? Those should stay identical to the upstream releases. The changes to the manual itself look useful. |
|
Sorry about the changes to |
|
Yes, much better! Did you make this with a script? If so, it would be nice to add it to CI as a check. |
|
@david-christiansen Yes, check out this! Would be great to have it in CI. Let me know if there is anything left to fix in this PR. |
|
The concrete changes are just fine, I simply like to include the thing that prevents future instances of a mistake along with the fixes to the mistakes. Codespell seems handy, I'll look at incorporating it. What about the double-space script that you used? |
|
OK, I think I won't get to setting up codespell in CI in the next few days, so let's merge this and open an issue. Thanks again! |
No description provided.