tools: add a tool to build and publish the documentation

Signed-off-by: Peter Hutterer <peter.hutterer@who-t.net>

diff --git a/tools/publish-doc b/tools/publish-doc
new file mode 100755 (executable)
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