Script that automatically rebuilds a github pages branch

github-pages.sh

#!/bin/sh

set -e

# !!!!
echo "*** REPLACE this with the line which builds docs"
# !!!!

echo "*** Docs built ***"
tmpdir=`mktemp -d /tmp/gh-pages-build.XXXXXX`
mv doc/** $tmpdir
rmdir doc
git checkout gh-pages
git rm -rf .
mv $tmpdir/** .
git add -Av .
git commit -m "Updated docs"
echo "*** gh-pages branch updated ***"
rmdir $tmpdir
git checkout -
echo "Run this to complete:"
echo "git push origin gh-pages:gh-pages"

See also https://gist.github.com/domenic/ec8b0fc8ab45f39403dd