X-Git-Url: https://git.immae.eu/?a=blobdiff_plain;f=scripts%2Fpushdoc.sh;h=34c811a7c94ef18da05dd1e056181e819465b024;hb=5f9250171a10c0d7fff8ef98996ef678d3267c0b;hp=ddab752466a0b3ede87dbd6effff2e51f397f56d;hpb=6f7c6d5a22aec4c237f00bae8f27a3877419537b;p=github%2Ffretlink%2Fhmacaroons.git

diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh
index ddab752..34c811a 100644
--- 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,12 +17,15 @@ 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
 # will be lost, since we are overwriting it.) We redirect any output to
 # /dev/null to hide any sensitive credential data that might otherwise be exposed.
+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