Force build removal

diff --git a/devscripts/release.sh b/devscripts/release.sh
index 543634ce13e49955f59506d5651ad16d375e4de9..bb3180b26cd2f4e29f65b0497a68430cbae7b160 100755 (executable)
--- 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!"