fixed push_whack_pop to also handle directories

diff --git a/scripts/core/functions.sh b/scripts/core/functions.sh
index d6beda886cd5326e00e268dc87d839eda5d165a6..fa924a74d40ea65e778c16552863266536857c43 100644 (file)
--- a/scripts/core/functions.sh
+++ b/scripts/core/functions.sh
@@ -473,7 +473,7 @@ if [ -z "$skip_all" ]; then
   {
     local dir="$1"; shift
     pushd "$dir" &>/dev/null
-    rm $* &>/dev/null
+    rm -rf $* &>/dev/null
     popd &>/dev/null
   }