From 5c4d73f4a3d497e51c9f377af2ea63d21c4c5555 Mon Sep 17 00:00:00 2001
From: Ruben Ayrapetyan <r.ayrapetyan@samsung.com>
Date: Thu, 30 Oct 2014 21:25:01 +0300
Subject: [PATCH] Fixing Ctrl-C handling in tools/push.sh.

---
 tools/push.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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