Closed matthias314 closed 2 years ago
Thanks for the corrections. Can you please set your user name in git. See https://docs.github.com/en/get-started/getting-started-with-git/setting-your-username-in-git for instructions and redo this commit. I can also redo this commit for you if you let me know what you set your user name to.
Merged. Thanks for the corrections.
This PR adds some command line options to the man page that are currently mentioned in the Texinfo file only. It also corrects a few typos and tries to distinguish between HTML/SGML tags and attributes (which are the parameters inside a tag). Actually, when the documentation speaks of skipping a tag, it probably means the HTML/SGML element between the start tag and the end tag. This terminology occurs both in the man page and the Texinfo file, however.
This patch is taken from the new TeX mode patch (and slightly updated) since it has nothing to do with the new TeX mode.