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/pidiff.git"
git fetch origin
git reset origin/gh-pages
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"