diff options
| -rwxr-xr-x | scripts/update_out | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/scripts/update_out b/scripts/update_out new file mode 100755 index 000000000..d3950cf60 --- /dev/null +++ b/scripts/update_out @@ -0,0 +1,21 @@ +#! /bin/bash +# Run given command application and update the contents of a given file. +# Will not change the file if its contents has not changed. +[[ $# -gt 1 ]] || { echo "Usage: ${0##*/} FILE COMMAND" >&2; exit 1; } +set -u +declare -r outfile="$1" +shift +if [[ ! -f $outfile ]]; then + $@ >$outfile + exit +fi + +declare -r newout=${outfile}.new +$@ >$newout +rc=$? +if cmp -s $newout $outfile; then + rm $newout +else + mv -f $newout $outfile +fi +exit $rc |