1 files changed, 20 insertions, 0 deletions
diff --git a/deploy-docs.sh b/deploy-docs.sh
new file mode 100755
index 0000000..c8f25ee
--- /dev/null
+++ b/deploy-docs.sh
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+set -o errexit -o nounset
+
+rev=$(git rev-parse --short HEAD)
+
+cd target/doc
+
+git init
+git config user.email 'FlashCat@users.noreply.github.com'
+git config user.name 'FlashCat'
+git remote add upstream "https://${GH_TOKEN}@github.com/${TRAVIS_REPO_SLUG}.git"
+git fetch upstream gh-pages
+git reset upstream/gh-pages
+
+touch .
+
+git add -A .
+git commit -m "rebuild pages at ${rev}"
+git push -q upstream HEAD:gh-pages