From 70006f64c8994bd4fa48f9ad3ab13c2d9501b8f4 Mon Sep 17 00:00:00 2001
From: Ben Klein <ben@silver-chalice.com>
Date: Fri, 31 Jul 2015 13:43:47 -0500
Subject: [PATCH] add 'ghpages' script

---
 ghpages.sh | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100755 ghpages.sh

diff --git a/ghpages.sh b/ghpages.sh
new file mode 100755
index 00000000..ed03e6ee
--- /dev/null
+++ b/ghpages.sh
@@ -0,0 +1,47 @@
+#!/bin/bash -x
+
+git remote set-url --push origin `git config remote.origin.url | sed -e 's/^git:/https:/'`
+
+if ! (git remote set-branches --add origin gh-pages && git fetch -q); then
+    echo "No gh-pages, so not syncing"
+    exit 0
+fi
+
+if ! [ -d docs/target/generated-docs ]; then
+    echo "No gh-pages sources in docs/target/generated-docs, so not syncing"
+    exit 0
+fi
+
+# Stash any outstanding changes
+###################################################################
+git diff-index --quiet HEAD
+dirty=$?
+if [ "$dirty" != "0" ]; then git stash; fi
+
+# Switch to gh-pages branch to sync it with master
+###################################################################
+git checkout gh-pages
+
+for f in docs/target/generated-docs/*; do
+    file=${f#docs/target/generated-docs/*}
+    if ! git ls-files -i -o --exclude-standard --directory | grep -q ^$file$; then
+        # Not ignored...
+        cp -rf $f .
+        git add -A $file
+    fi
+done
+
+git commit -a -m "Sync docs from master to gh-pages"
+
+# Uncomment the following push if you want to auto push to
+# the gh-pages branch whenever you commit to master locally.
+# This is a little extreme. Use with care!
+###################################################################
+#git push origin gh-pages
+
+# Finally, switch back to the master branch and exit block
+git checkout master
+if [ "$dirty" != "0" ]; then git stash pop; fi
+
+exit 0
+