diff options
| -rw-r--r-- | doc/info/content.texinfo | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/info/content.texinfo b/doc/info/content.texinfo index 9617f69..327d998 100644 --- a/doc/info/content.texinfo +++ b/doc/info/content.texinfo @@ -1,8 +1,10 @@ @c This file includes everything after the titlepage. +@ifnothtml @c @shortcontents @c (if the table of content gets too large.) @contents +@end ifnothtml @menu |