Fix commented out git push

Otherwise the result is not persisted
2016-09-22 12:03:14 +01:00
parent 96e92e5dd4
commit 26a0e7df3d
1 changed files with 1 additions and 1 deletions
--- a/docs/src/main/asciidoc/ghpages.sh
+++ b/docs/src/main/asciidoc/ghpages.sh
@@ -239,7 +239,7 @@ function commit_changes_if_applicable() {
        # This is a little extreme. Use with care!
        ###################################################################
        if [[ "${COMMIT_SUCCESSFUL}" == "yes" ]] ; then
-            echo git push origin gh-pages
+            git push origin gh-pages
        fi
    fi
 }