diff options
Diffstat (limited to 'doc')
-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 |