1 files changed, 8 insertions, 0 deletions
diff --git a/tool/ifchange b/tool/ifchange
index 544513ad15..8bfca26703 100755
--- a/tool/ifchange
+++ b/tool/ifchange
@@ -1,6 +1,11 @@
 #!/bin/sh
 # usage: ifchange target temporary
 
+unset timestamp
+if [ "$1" = --timestamp ]; then
+    timestamp=yes
+    shift
+fi
 target="$1"
 temp="$2"
 if [ "$temp" = - ]; then
@@ -15,3 +20,6 @@ else
     echo "$target updated"
     mv -f "$temp" "$target"
 fi
+if [ $timestamp ]; then
+    touch `dirname "$target"`/.time.`basename "$target"`
+fi