diff options
author | Mario Mulansky <mario.mulansky@gmx.net> | 2014-10-24 10:28:04 +0200 |
---|---|---|
committer | Mario Mulansky <mario.mulansky@gmx.net> | 2014-10-24 10:28:04 +0200 |
commit | 874d980976169baf9ec01f8ff4ee1c218a447077 (patch) | |
tree | 2e31478805a861c40e7884038b3942a19c597252 | |
parent | 8ba04b660dc3213ab6e5f1e839558d9fc692660d (diff) |
+update website script
-rwxr-xr-x | doc/copy_html | 12 |
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 |