diff --git a/tools/publish-doc b/tools/publish-doc new file mode 100755 index 0000000..66777ab --- /dev/null +++ b/tools/publish-doc @@ -0,0 +1,11 @@ +#!/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