tools/copy-if-change

# Like cp $1 $2, but if the files are the same, do NOTHING.
# Status is 0 if $2 is changed, 1 otherwise.

if test -r "$2"; then
  if cmp "$1" "$2" > /dev/null; then
    echo "$2" is unchanged
  else
    cp -f "$1" "$2"
  fi
else
  cp "$1" "$2"
fi