aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-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