diff options
Diffstat (limited to 'doc/sidebar.awk')
| -rw-r--r-- | doc/sidebar.awk | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/sidebar.awk b/doc/sidebar.awk index a8d25bf9..bb381aa3 100644 --- a/doc/sidebar.awk +++ b/doc/sidebar.awk @@ -20,11 +20,11 @@ # Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA BEGIN { - print "% *****************************************************" - print "% * DO NOT MODIFY THIS FILE!!!! *" - print "% * It was generated from gawkman.texi by sidebar.awk *" - print "% * Edit gawkman.texi instead. *" - print "% *****************************************************" + print "% ****************************************************" + print "% * DO NOT MODIFY THIS FILE!!!! *" + print "% * It was generated from gawktexi.in by sidebar.awk *" + print "% * Edit gawktexi.in instead. *" + print "% ****************************************************" } /^@sidebar/ { |