-# m4 wrapper which uses $1.m4 as template file, feeds it to m4 and writes it
-# to $1 with a warning at the beginning to not edit the generated file.
+# Write a warning to $1 to make clear it should not be modified. $2 is the
+# source for the generated file. Also print a message to stdout that the file
+# $1 was generated from $2 using the command $3 with options $4.
+warning() {
+ echo "###################################" > $1
+ echo "# WARNING! DO NOT EDIT THIS FILE! #" >> $1
+ echo "###################################" >> $1
+ echo >> $1
+ echo "# It was generated from $2 on `date`." >> $1
+ echo >> $1
+
+ # Display given options if there were any (zsh has a problem with $options
+ # as variable name).
+ option=
+ if [ -n "$4" ]; then
+ option=" with options '$4'"
+ fi
+ # Write message to stdout.
+ echo "$3: generating '$1' from '$2'$option"
+
+ unset option
+}
+
+# Generate a file using several methods. A warning not to edit it is
+# automatically added to the created file and a message printed to stdout
+# through warning().
+#
+# The following commands are possible; the file extension for the source file
+# in brackets.