Browse Source

devel: dont update devel.php if unchanged

master
Xuefer 6 years ago
parent
commit
10fcce4917
  1. 7
      devel/run

7
devel/run

@ -340,7 +340,12 @@ run() {
< "$1" \
sed -r -e 's#__#____#g' \
| cpp -C -P -traditional-cpp -undef -ffreestanding -DPHP_VERSION=$phpVersion \
| sed -r -e 's#^ +##g' -e 's#\t +#\t#g' -e 's#____#__#g' > devel.php || exit $?
| sed -r -e 's#^ +##g' -e 's#\t +#\t#g' -e 's#____#__#g' > devel.php.tmp || exit $?
if [[ ! -e devel.php ]] || ! cmp devel.php.tmp devel.php >/dev/null; then
cat devel.php.tmp > devel.php
else
rm -f devel.php.tmp
fi
shift
set -- devel.php "$@"
;;

Loading…
Cancel
Save