scripts/pushdoc.sh

   1 #!/bin/bash
   2 set -e # exit with nonzero exit code if anything fails
   3
   4 # Build documentation
   5 cabal haddock
   6
   7 # Copy benchmark
   8 cp benchmark.html dist/doc/html/hmacaroons
   9
  10 # Go to haddock output dir
  11 cd dist/doc/html/hmacaroons
  12
  13 # Quiet the git init message, since it's not useful in the build log
  14 git init > /dev/null 2>&1
  15
  16 # inside this git repo we'll pretend to be a new user
  17 git config user.name "Travis CI"
  18 git config user.email "julien.tanguy@jhome.fr"
  19
  20 # The first and only commit to this new Git repo contains all the
  21 # files present with the commit message "Deploy to GitHub Pages".
  22 git add .
  23 # Silence the commit too
  24 git commit -m "Deploy to GitHub Pages" > /dev/null 2>&1
  25
  26
  27 # Force push from the current repo's master branch to the remote
  28 # repo's gh-pages branch. (All previous history on the gh-pages branch
  29 # will be lost, since we are overwriting it.) We redirect any output to
  30 # /dev/null to hide any sensitive credential data that might otherwise be exposed.
  31 echo "Pushing haddock to gh-pages"
  32 git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1
  33
  34 cd ~/build/jtanguy/hmacaroons