diff options
author | Paul Eggert <[email protected]> | 2012-08-13 20:15:52 -0700 |
---|---|---|
committer | Paul Eggert <[email protected]> | 2012-08-13 20:15:52 -0700 |
commit | 76d0e68f8d6bbae0886443c98322e81eab0dc5aa (patch) | |
tree | ff409b56c98820ef49f74dc20a5a27fa7cb76052 /doc | |
parent | 5884c3244a764191661ee8d908229be0260336dc (diff) |
Merge from gnulib.
This incorporates:
2012-08-05 extern-inline: also ignore -Wmissing-declarations
Diffstat (limited to 'doc')
-rw-r--r-- | doc/misc/texinfo.tex | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/doc/misc/texinfo.tex b/doc/misc/texinfo.tex index c7354edcaf..dc4bf6400c 100644 --- a/doc/misc/texinfo.tex +++ b/doc/misc/texinfo.tex @@ -3146,12 +3146,17 @@ end % hopefully nobody will notice/care. \edef\ecsize{\csname\curfontsize ecsize\endcsname}% \edef\nominalsize{\csname\curfontsize nominalsize\endcsname}% - \ifx\curfontstyle\bfstylename - % bold: - \font\thisecfont = ecb\ifusingit{i}{x}\ecsize \space at \nominalsize + \ifmonospace + % typewriter: + \font\thisecfont = ectt\ecsize \space at \nominalsize \else - % regular: - \font\thisecfont = ec\ifusingit{ti}{rm}\ecsize \space at \nominalsize + \ifx\curfontstyle\bfstylename + % bold: + \font\thisecfont = ecb\ifusingit{i}{x}\ecsize \space at \nominalsize + \else + % regular: + \font\thisecfont = ec\ifusingit{ti}{rm}\ecsize \space at \nominalsize + \fi \fi \thisecfont } |