On Sun, Dec 04, 2022 at 02:17:10PM +0000, Werner LEMBERG wrote: > Hmm. Because the code gets translated from Texinfo to LaTeX it should > be possible to simply use `\texttt` (or something similar) with > properly escaped characters, no?
Yes, it would have been possible to have done it that way.
