diff options
| -rw-r--r-- | doc/sh-utils.texi | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sh-utils.texi b/doc/sh-utils.texi index 796d050ea..6b9376c8a 100644 --- a/doc/sh-utils.texi +++ b/doc/sh-utils.texi @@ -113,7 +113,7 @@ by the Foundation. @end titlepage -@ifinfo +@ifnottex @node Top @top GNU shell utilities @@ -140,7 +140,7 @@ This manual documents version @value{VERSION} of the GNU shell utilities. * Index:: General index. @end menu -@end ifinfo +@end ifnottex @node Introduction |