X-Git-Url: https://ruderich.org/simon/gitweb/?a=blobdiff_plain;f=lib.sh;h=e9fd56dbed9facaa46da77390a738d922989db4a;hb=732dfd2898effb21d6dd341c7d5b65962556fa1d;hp=fbef907d330bd62aec6bf67a5d0b4c237c267159;hpb=2b996dfbed52a0ec1592b4820990f97b5147b2d4;p=config%2Fdotfiles.git

diff --git a/lib.sh b/lib.sh
index fbef907..e9fd56d 100644
--- a/lib.sh
+++ b/lib.sh
@@ -71,7 +71,7 @@ link() {
 
 # 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
@@ -80,12 +80,21 @@ warning() {
     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.
@@ -117,7 +126,7 @@ generate() {
     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"