# 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.
+# $1 was generated from $2 using the command $3 with options $4.
warning() {
echo "###################################" > $1
echo "# WARNING! DO NOT EDIT THIS FILE! #" >> $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'"
+ echo "$3: generating '$1' from '$2'$option"
+
+ unset option
}
# Generate a file using several methods. A warning is automatically added to
fi
# Add warning to file and write a message to stdout.
- warning "$file" "$file$extension" $command
+ warning "$file" "$file$extension" $command "$*"
# Generate $file from $file$extension using the given command.
cat "$file$extension" | $command "$@" >> "$file"