diff options
| author | Mario Mulansky <mario.mulansky@gmx.net> | 2014-10-24 10:28:51 +0200 |
|---|---|---|
| committer | Mario Mulansky <mario.mulansky@gmx.net> | 2014-10-24 10:28:51 +0200 |
| commit | 0261baf17427d854bdd7368e0a4e5ef8c0997d25 (patch) | |
| tree | b821172b56305ec40af699b9715cb2d761ba06a4 /doc/update_website | |
| parent | 874d980976169baf9ec01f8ff4ee1c218a447077 (diff) | |
renamed update website script
Diffstat (limited to 'doc/update_website')
| -rwxr-xr-x | doc/update_website | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/update_website b/doc/update_website new file mode 100755 index 0000000..1be8f05 --- /dev/null +++ b/doc/update_website @@ -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 |