diff options
| -rwxr-xr-x | doc/update_website | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/update_website b/doc/update_website index 1be8f05..dc73f49 100755 --- a/doc/update_website +++ b/doc/update_website @@ -5,7 +5,7 @@ rc=$? if [[ $rc != 0 ]] ; then exit $rc fi -cp -r _build/html/*.html _build/html/*.js _build/html/_static ../ +cp -r _build/html/*.html _build/html/*.js _build/html/_static _build/html/_modules ../ echo "html files copied" git commit -am"website update" git push |