diff --git a/misc/tools-source/install_wrapper.sh b/misc/tools-source/install_wrapper.sh index 128980ad2..05a3a1c4c 100644 --- a/misc/tools-source/install_wrapper.sh +++ b/misc/tools-source/install_wrapper.sh @@ -42,6 +42,12 @@ while [ $# -gt 0 ]; do newcommand="$newcommand $1 $2" shift 1 ;; + -s|--strip) + if [[ "$ROCKCFG_DEBUG" = 0 || $command != *install ]] + then + newcommand="$newcommand $1" + fi + ;; -*) newcommand="$newcommand $1" ;;