summaryrefslogtreecommitdiffstats
path: root/third_party/rust/bit-set/deploy-docs.sh
diff options
context:
space:
mode:
Diffstat (limited to 'third_party/rust/bit-set/deploy-docs.sh')
-rw-r--r--third_party/rust/bit-set/deploy-docs.sh20
1 files changed, 20 insertions, 0 deletions
diff --git a/third_party/rust/bit-set/deploy-docs.sh b/third_party/rust/bit-set/deploy-docs.sh
new file mode 100644
index 0000000000..c8f25ee86b
--- /dev/null
+++ b/third_party/rust/bit-set/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