-# 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 test -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().
+# Generate a file from a source file using a given command. A warning not to
+# edit it is automatically added to the created file.