diff options
Diffstat (limited to 'devscripts/release.sh')
| -rwxr-xr-x | devscripts/release.sh | 2 | 
1 files changed, 1 insertions, 1 deletions
| diff --git a/devscripts/release.sh b/devscripts/release.sh index 543634ce1..bb3180b26 100755 --- a/devscripts/release.sh +++ b/devscripts/release.sh @@ -81,6 +81,6 @@ ROOT=$(pwd)      git push "$ROOT" gh-pages      git push "$ORIGIN_URL" gh-pages  ) -rm -r build +rm -rf build  echo "\n### DONE!" | 
