1 files changed, 24 insertions, 0 deletions

diff --git a/scripts/pushdoc.sh b/scripts/pushdoc.sh
new file mode 100644
index 0000000..ddab752
--- /dev/null
+++ b/scripts/pushdoc.sh
@@ -0,0 +1,24 @@
+#!/bin/bash
+set -e # exit with nonzero exit code if anything fails
+
+cabal haddock
+
+pushd dist/doc/html/hmacaroons
+git init
+
+# inside this git repo we'll pretend to be a new user
+git config user.name "Travis CI"
+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"
+
+# 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.
+git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1
+
+popd