+# Write a warning to $1 to make clear it should not be modified. $2 is the
+# source for the generated file.
+setup_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
+}
+