scripts/push-docs

#!/bin/bash
set -e
set -o pipefail

if [ "${CIRCLE_BRANCH}" != "master" ] || [ "${CIRCLE_PULL_REQUEST}" != "" ]; then
  echo "Docs would now be pushed, if this were submitted to master."
  exit 0
fi

rev=$(git rev-parse --short HEAD)

# Copy circle config under docs build so that circle knows to ignore gh-pages branch
cp -rv .circleci docs/_build

cd docs/_build

git init
git config user.name "Rohan McGovern"
git config user.email "rohan@mcgovern.id.au"

# If it's asking for a password, something is wrong.
export GIT_ASKPASS=false

{
  git remote add origin "https://$GITHUB_TOKEN:@github.com/rohanpm/more-executors.git"
  git fetch origin
  git reset origin/gh-pages

  # Create CNAME file here if needed, e.g.
  # echo myho.st > CNAME

  git add -A .
  git commit -m "Build documentation at ${rev}"
  git push -q origin HEAD:refs/heads/gh-pages
} 2>&1 | sed -e "s|$GITHUB_TOKEN|xxxxxx|g"