diff options
| -rw-r--r-- | texinfo.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/texinfo.tex b/texinfo.tex index 759e3c1..7614465 100644 --- a/texinfo.tex +++ b/texinfo.tex @@ -1197,7 +1197,7 @@ where each line of input produces a line of output.} \def\key#1{{\smallrm\textfont2=\smallsy \leavevmode\hbox{% \raise0.4pt\hbox{$\langle$}\kern-.08em\vtop{% \vbox{\hrule\kern-0.4pt - \hbox{\raise0.4pt\hbox{\vphantom{$\langle$}}\uppercase{#1}}}% + \hbox{\raise0.4pt\hbox{\vphantom{$\langle$}}#1}}% \kern-0.4pt\hrule}% \kern-.06em\raise0.4pt\hbox{$\rangle$}}}} %\def\key #1{{\ttsl \nohyphenation \uppercase{#1}}\null} |