diff options
Diffstat (limited to 'doc/info/reusable/paper.texinfo')
| -rw-r--r-- | doc/info/reusable/paper.texinfo | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/info/reusable/paper.texinfo b/doc/info/reusable/paper.texinfo index 1fc9f0f..5a6aca8 100644 --- a/doc/info/reusable/paper.texinfo +++ b/doc/info/reusable/paper.texinfo @@ -75,7 +75,9 @@ @fonttextsize 10 @end ifset @ifclear SMALLFONT +@iftex @c Because of bug in Texinfo<=4.13 @fonttextsize 11 +@end iftex @end ifclear @c In America it is customary to have two spaces after |