no push in ant script

This commit is contained in:
Jindra Petřík
2014-11-11 10:24:51 +01:00
parent baac7dd608
commit eb612dc14d

View File

@@ -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">