summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/push-ghpages12
1 files changed, 12 insertions, 0 deletions
diff --git a/tools/push-ghpages b/tools/push-ghpages
new file mode 100644
index 0000000..91f606a
--- /dev/null
+++ b/tools/push-ghpages
@@ -0,0 +1,12 @@
+#!/bin/bash
+set -e -o pipefail
+
+./generate-docs
+git checkout gh-pages
+find . -maxdepth 1 -not -name "docs" -not -name ".git" -print0 | xargs -0 rm -r
+mv docs/* .
+mv docs/.nojekyll .
+rmdir docs
+git add -A
+git commit -m "Updated docs $(date)"
+git push origin gh-pages