agda-mode-vscode icon indicating copy to clipboard operation
agda-mode-vscode copied to clipboard

"Shortcut" is typoed as "Shortcurs"

Open pragma- opened this issue 2 years ago • 2 comments

Just a quick heads-up to let you know that in the Visual Studio Marketplace description, I noticed "Shortcut" was typoed as "Shortcurs". I see the same typo here in the README.md.

pragma- avatar Jun 18 '22 20:06 pragma-

I have a question. Would it have been appropriate to create a PR for a simple one-word typofix? It seems to me that you would think I was trying to add my name to the list of contributors without having made any significant contribution. I felt that creating an issue would be the least invasive way to let you know of this typo. I'd like to know your thoughts on this. If I had made a PR would it have annoyed you or would you have happily accepted it?

pragma- avatar Jun 18 '22 20:06 pragma-

Thank you for reporting this. It'd be great if you can make a PR ❤️!

banacorn avatar Aug 06 '22 09:08 banacorn

Sure thing. PR #114 fixes the typo. My editor and git both complained about trailing whitespace on some lines, so I cleaned those up too.

pragma- avatar Aug 09 '22 03:08 pragma-