diff options
| -rwxr-xr-x | readline/history.texi | 8 | ||||
| -rwxr-xr-x | readline/readline.texi | 8 |
2 files changed, 12 insertions, 4 deletions
diff --git a/readline/history.texi b/readline/history.texi index 7302edb..1bcce4d 100755 --- a/readline/history.texi +++ b/readline/history.texi @@ -1,9 +1,13 @@ \input texinfo.tex @setfilename history.info -@c start-menu +@ifinfo +@format +START-INFO-DIR-ENTRY * History: (history). The GNU History library. -@c end-menu +END-INFO-DIR-ENTRY +@end format +@end ifinfo @ifinfo This file documents the GNU History library. diff --git a/readline/readline.texi b/readline/readline.texi index 578e1b7..ea6c9ea 100755 --- a/readline/readline.texi +++ b/readline/readline.texi @@ -5,9 +5,13 @@ @comment %**end of header (This is for running Texinfo on a region.) @synindex fn vr -@c start-menu +@ifinfo +@format +START-INFO-DIR-ENTRY * Readline: (readline). The GNU Readline Library. -@c end-menu +END-INFO-DIR-ENTRY +@end format +@end ifinfo @iftex @comment finalout |