1 files changed, 33 insertions, 0 deletions
diff --git a/website/publish b/website/publish
new file mode 100755
index 00000000..4894c4e7
--- /dev/null
+++ b/website/publish
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+CURDIR=`pwd`
+
+
+cd `dirname $0` || exit
+cd .. || exit
+
+if [ ! -e dist/website.zip ]; then
+	echo There is no dist/website.zip file! Run:
+	echo ant website
+	echo then restart this script
+	exit
+fi
+
+mkdir -p build/temp || exit
+cd build/temp || exit
+git clone -l -n ../.. websitegit || exit
+cd websitegit || exit
+git branch gh-pages origin/gh-pages || exit
+git checkout gh-pages || exit
+rm -r * || exit
+unzip ../../../dist/website.zip || exit
+git add . || exit
+git commit -a -m website || exit
+git push origin gh-pages || exit
+cd .. || exit
+rm -rf websitegit || exit
+
+cd "$CURDIR"
+
+echo Your gh-pages branch has been updated. Do not forget to run:
+echo git push origin gh-pages