summaryrefslogtreecommitdiff
path: root/tools/publish-doc
blob: 66777ab3add0c23388870c3b4bec083190b75fc9 (plain)
1
2
3
4
5
6
7
8
9
10
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