diff --git a/tools/push.sh b/tools/push.sh index 155568e6d..b2c96532c 100755 --- a/tools/push.sh +++ b/tools/push.sh @@ -55,13 +55,9 @@ echo for commit_hash in $commits_to_push do - echo " > Testing $commit_hash" - echo -n " > " - git log --pretty=format:"%H %s" | grep $commit_hash | grep -o " .*" - echo - git checkout $commit_hash >&/dev/null status_code=$? + if [ $status_code -ne 0 ] then echo "git checkout $commit_hash failed" @@ -69,6 +65,11 @@ do exit 1 fi + echo " > Testing $commit_hash" + echo -n " > " + git log --pretty=format:"%H %s" | grep $commit_hash | grep -o " .*" + echo + make -j precommit 2>&1 status_code=$? if [ $status_code -ne 0 ]