+update website script

1 files changed, 12 insertions, 0 deletions

diff --git a/doc/copy_html b/doc/copy_html
new file mode 100755
index 0000000..1be8f05
--- /dev/null
+++ b/doc/copy_html
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+git checkout gh-pages
+rc=$?
+if [[ $rc != 0 ]] ; then
+    exit $rc
+fi
+cp -r _build/html/*.html _build/html/*.js _build/html/_static ../
+echo "html files copied"
+git commit -am"website update"
+git push
+git checkout master