diff --git a/tools/push.sh b/tools/push.sh index 28ac2b4c8..c2b1a62ec 100755 --- a/tools/push.sh +++ b/tools/push.sh @@ -74,7 +74,8 @@ function ctrl_c() { # git notes --ref=perf remove $commit_hash # git notes --ref=mem remove $commit_hash # done -# exit 1 + + exit 1 } echo