diff options
Diffstat (limited to 'manual/header.texi')
| -rw-r--r-- | manual/header.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/manual/header.texi b/manual/header.texi index 0ab36d7e5e..7a4cb058fc 100644 --- a/manual/header.texi +++ b/manual/header.texi @@ -10,7 +10,7 @@ it. @c This table runs wide. Shrink fonts. @iftex -@indexfonts @rm +@smallfonts @rm @end iftex @table @code @comment summary.texi is generated from the other Texinfo files. |