diff options
Diffstat (limited to 'src/mkheader.awk')
| -rw-r--r-- | src/mkheader.awk | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/mkheader.awk b/src/mkheader.awk index 0d09a8c..0ff08f9 100644 --- a/src/mkheader.awk +++ b/src/mkheader.awk @@ -71,11 +71,12 @@ BEGIN { extra_body = 0; gpg_error_h = 0; - print "/* Output of mkheader.awk. DO NOT EDIT. */"; + print "/* Output of mkheader.awk. DO NOT EDIT. -*- buffer-read-only: t -*- */"; print ""; } + sources_header { if ($1 ~ /^[0123456789]+$/) { |