diff options
Diffstat (limited to 'manual/header.texi')
| -rw-r--r-- | manual/header.texi | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/manual/header.texi b/manual/header.texi index 066fdbf1aa..b6ca60ee96 100644 --- a/manual/header.texi +++ b/manual/header.texi @@ -7,8 +7,15 @@ standard or other source from which each facility is derived, and tells you where in the manual you can find more information about how to use it. +@c This table runs wide. Shrink fonts. +@iftex +@indexfonts @rm +@end iftex @table @code @comment summary.texi is generated from the other Texinfo files. @comment See the Makefile and summary.awk for the details. @include summary.texi @end table +@iftex +@textfonts @rm +@end iftex |