#!/bin/bash

git checkout master
make
mv doc/html doc/publish
git checkout gh-pages
rm -rf doc/html
mv doc/publish doc/html
git add doc/html
git commit -asm "Documentation update for `git log -n 1 --format="format:%h" master`"
git checkout master