Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

manual: LaTeX collapses double dashes in command-line options since 4.08 #10513

Closed
wikku opened this issue Jul 15, 2021 · 2 comments
Closed

manual: LaTeX collapses double dashes in command-line options since 4.08 #10513

wikku opened this issue Jul 15, 2021 · 2 comments

Comments

@wikku
Copy link
Contributor

wikku commented Jul 15, 2021

image
--help is rendered -help

This could have been introduced by loading fontenc in #1789.

In tex source code it's \machine{--help}. \machine is \tt with adjusted spacing (?). Probably it should be \verb instead, but I don't understand these 25 year old macros well.
@wikku wikku changed the title manual: LaTeX collapses double dashes since 4.08 manual: LaTeX collapses double dashes in command-line options since 4.08 Jul 15, 2021
@xavierleroy
Copy link
Contributor

I agree \verb should be used instead of \machine in the hand-written LaTeX sources (.etex files).

\machine is also generated by the texquote2 preprocessor, and there might be reasons for not using \verb there (such as robustness in all contexts).

@xavierleroy
Copy link
Contributor

This said, I see no point for ligatures in a typewriter font. (Yes, -- for en-dash is part of TeX's ligature machinery.) So, turning ligatures off for \tt would be a good fix.

xavierleroy added a commit to xavierleroy/ocaml that referenced this issue Jul 16, 2021
@xavierleroy
Disable ligatures in typewriter fonts
e74a533 
Because `--help` should be rendered with two minus signs, not one dash.

Use the "microtype" package for this purpose.

Fixes: ocaml#10513
@xavierleroy xavierleroy mentioned this issue Jul 16, 2021
Merged
@gasche gasche closed this as completed in 265bba9 Jul 19, 2021
@wikku wikku mentioned this issue Sep 6, 2021
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@xavierleroy @wikku