diff options
Diffstat (limited to 'doc/gawk.texi')
| -rw-r--r-- | doc/gawk.texi | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/gawk.texi b/doc/gawk.texi index acd2b143..7c53fc14 100644 --- a/doc/gawk.texi +++ b/doc/gawk.texi @@ -1,8 +1,8 @@ -% ***************************************************** -% * DO NOT MODIFY THIS FILE!!!! * -% * It was generated from gawkman.texi by sidebar.awk * -% * Edit gawkman.texi instead. * -% ***************************************************** +% **************************************************** +% * DO NOT MODIFY THIS FILE!!!! * +% * It was generated from gawktexi.in by sidebar.awk * +% * Edit gawktexi.in instead. * +% **************************************************** \input texinfo @c -*-texinfo-*- @c vim: filetype=texinfo @c %**start of header (This is for running Texinfo on a region.) |