Silence git messages in pushdoc.sh

diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh
index bea97f028a23fb91968f308d219f6679bb464c93..34c811a7c94ef18da05dd1e056181e819465b024 100644 (file)
--- a/scripts/pushdoc.sh
+++ b/scripts/pushdoc.sh
@@ -1,10 +1,14 @@
 #!/bin/bash
 set -e # exit with nonzero exit code if anything fails
 
+# Build documentation
 cabal haddock
 
-pushd dist/doc/html/hmacaroons
-git init
+# Go to haddock output dir
+cd dist/doc/html/hmacaroons
+
+# Quiet the git init message, since it's not useful in the build log
+git init > /dev/null 2>&1
 
 # inside this git repo we'll pretend to be a new user
 git config user.name "Travis CI"
@@ -13,7 +17,9 @@ git config user.email "julien.tanguy@jhome.fr"
 # The first and only commit to this new Git repo contains all the
 # files present with the commit message "Deploy to GitHub Pages".
 git add .
-git commit -m "Deploy to GitHub Pages"
+# Silence the commit too
+git commit -m "Deploy to GitHub Pages" > /dev/null 2>&1
+
 
 # Force push from the current repo's master branch to the remote
 # repo's gh-pages branch. (All previous history on the gh-pages branch
@@ -22,4 +28,4 @@ git commit -m "Deploy to GitHub Pages"
 echo "Pushing haddock to gh-pages"
 git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1
 
-popd
+cd ~/build/jtanguy/hmacaroons