Merge branch 'bugfix'

This commit is contained in:
Ihor Radchenko 2023-04-20 11:05:12 +02:00
commit 9440a29828
No known key found for this signature in database
GPG Key ID: 6470762A7DA11D8B
1 changed files with 3 additions and 1 deletions

View File

@ -1838,9 +1838,11 @@ INFO is a plist used as a communication channel. See
"Protect special chars, then wrap TEXT in \"\\texttt{}\"."
(format "\\texttt{%s}"
(replace-regexp-in-string
"--\\|[\\{}$%&_#~^]"
"--\\|<<\\|>>\\|[\\{}$%&_#~^]"
(lambda (m)
(cond ((equal m "--") "-{}-{}")
((equal m "<<") "<{}<{}")
((equal m ">>") ">{}>{}")
((equal m "\\") "\\textbackslash{}")
((equal m "~") "\\textasciitilde{}")
((equal m "^") "\\textasciicircum{}")