From eb612dc14d422bf5a969a610bc3bb5d3000b026d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jindra=20Pet=C5=99=C3=ADk?= <jindra.petrik@gmail.com>
Date: Tue, 11 Nov 2014 10:24:51 +0100
Subject: [PATCH] no push in ant script

---
 build_common.xml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/build_common.xml b/build_common.xml
index 03ce5e641..378e077b4 100644
--- a/build_common.xml
+++ b/build_common.xml
@@ -584,8 +584,7 @@
     </target>
     
     <target name="git-push">
-        <!-- TODO -->
-        <echo>WARNING: Changes need to be PUSHed to the GIT repository.</echo>
+        <!-- NOTHING -->       
     </target>
     
     <target name="-git-commit-versioninfo">