# Get all necessary paths.
pwd=`pwd`
base=`dirname "$2"`
- source=`echo -n "$pwd/$1" | sed "s|$base/||"`
+ source=`echo "$pwd/$1" | sed "s|$base/||"`
target=`basename "$2"`
# Go to the directory where the link is going to be created.
# 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
-# the created file and a message printed to stdout through warning().
+# 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.
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"