Only push to bytecode repository if there is something to push.

This commit is contained in:
chriseth 2017-07-03 18:25:37 +02:00
parent 76d3b7c5a1
commit 066e995bbd

View File

@ -98,9 +98,8 @@ EOF
REPORT="$DIRNAME/$ZIP_SUFFIX.txt" REPORT="$DIRNAME/$ZIP_SUFFIX.txt"
cp ../report.txt "$REPORT" cp ../report.txt "$REPORT"
# Only push if adding actually worked, i.e. there were changes. # Only push if adding actually worked, i.e. there were changes.
if git add "$REPORT" if git add "$REPORT" && git commit -a -m "Added report $REPORT"
then then
git commit -a -m "Added report $REPORT"
git pull --rebase git pull --rebase
git push origin git push origin
else else