aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorJulien Tanguy <julien.tanguy@jhome.fr>2015-09-05 02:48:19 +0200
committerJulien Tanguy <julien.tanguy@jhome.fr>2015-09-05 02:48:19 +0200
commit5250177ea4b0a375bc5b6414383f03072ed3df01 (patch)
tree466ecae41b1c8d60fa3aba77b1c41f14ae8457b9
parent15b8a37d5030deaa7625d6c9a62671a8368e5a78 (diff)
downloadhmacaroons-5250177ea4b0a375bc5b6414383f03072ed3df01.tar.gz
hmacaroons-5250177ea4b0a375bc5b6414383f03072ed3df01.tar.zst
hmacaroons-5250177ea4b0a375bc5b6414383f03072ed3df01.zip
Silence git messages in pushdoc.sh
-rw-r--r--scripts/pushdoc.sh14
1 files changed, 10 insertions, 4 deletions
diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh
index bea97f0..34c811a 100644
--- a/scripts/pushdoc.sh
+++ b/scripts/pushdoc.sh
@@ -1,10 +1,14 @@
1#!/bin/bash 1#!/bin/bash
2set -e # exit with nonzero exit code if anything fails 2set -e # exit with nonzero exit code if anything fails
3 3
4# Build documentation
4cabal haddock 5cabal haddock
5 6
6pushd dist/doc/html/hmacaroons 7# Go to haddock output dir
7git init 8cd dist/doc/html/hmacaroons
9
10# Quiet the git init message, since it's not useful in the build log
11git init > /dev/null 2>&1
8 12
9# inside this git repo we'll pretend to be a new user 13# inside this git repo we'll pretend to be a new user
10git config user.name "Travis CI" 14git config user.name "Travis CI"
@@ -13,7 +17,9 @@ git config user.email "julien.tanguy@jhome.fr"
13# The first and only commit to this new Git repo contains all the 17# The first and only commit to this new Git repo contains all the
14# files present with the commit message "Deploy to GitHub Pages". 18# files present with the commit message "Deploy to GitHub Pages".
15git add . 19git add .
16git commit -m "Deploy to GitHub Pages" 20# Silence the commit too
21git commit -m "Deploy to GitHub Pages" > /dev/null 2>&1
22
17 23
18# Force push from the current repo's master branch to the remote 24# Force push from the current repo's master branch to the remote
19# repo's gh-pages branch. (All previous history on the gh-pages branch 25# repo's gh-pages branch. (All previous history on the gh-pages branch
@@ -22,4 +28,4 @@ git commit -m "Deploy to GitHub Pages"
22echo "Pushing haddock to gh-pages" 28echo "Pushing haddock to gh-pages"
23git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1 29git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1
24 30
25popd 31cd ~/build/jtanguy/hmacaroons