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 2a551cd6e1..ce661df43b 100644 --- a/manual/header.texi +++ b/manual/header.texi @@ -14,7 +14,7 @@ it. @end iftex @table @code @comment summary.texi is generated from the other Texinfo files. -@comment See the Makefile and summary.awk for the details. +@comment See the Makefile and summary.pl for the details. @include summary.texi @end table @iftex |