wrong font in @shortcontents

[Werner LEMBERG]

The following patch fixes an incorrect font size for the \tt font in
@shortcontents (for my document, it was 2pt too big).  This is for
texinfo 4.2.


    Werner


======================================================================


--- texinfo.tex~        Tue Apr 23 22:09:09 2002
+++ texinfo.tex Thu May  2 15:04:36 2002
@@ -1345,6 +1345,7 @@
 \setfont\shortcontrm\rmshape{12}{1000}
 \setfont\shortcontbf\bxshape{12}{1000}
 \setfont\shortcontsl\slshape{12}{1000}
+\setfont\shortconttt\ttshape{12}{1000}
 
 %% Add scribe-like font environments, plus @l for inline lisp (usually sans
 %% serif) and @ii for TeX italic
@@ -4007,7 +4008,8 @@
       \let\unnumbchapentry = \shortunnumberedentry
       % We want a true roman here for the page numbers.
       \secfonts
-      \let\rm=\shortcontrm \let\bf=\shortcontbf \let\sl=\shortcontsl
+      \let\rm=\shortcontrm \let\bf=\shortcontbf
+      \let\sl=\shortcontsl \let\tt=\shortconttt
       \rm
       \hyphenpenalty = 10000
       \advance\baselineskip by 1pt % Open it up a little.