Fixing Ctrl-C handling in tools/push.sh.

2014-10-30 21:25:01 +03:00
parent bc484e2048
commit 5c4d73f4a3
1 changed files with 2 additions and 1 deletions
@@ -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