From: Fabian Castelli Date: Mon, 7 Jun 2021 15:16:50 +0000 (+0200) Subject: Update prefix option handling X-Git-Tag: v9.3.3-r1~1^2~32^2 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fpull%2F210%2Fhead;p=candi.git Update prefix option handling --- diff --git a/candi.sh b/candi.sh index 7658a24..2104cd8 100755 --- a/candi.sh +++ b/candi.sh @@ -71,8 +71,6 @@ while [ -n "$1" ]; do ;; -p=*|--prefix=*) PREFIX="${param#*=}" - # replace '~' by $HOME - PREFIX=${PREFIX/#~\//$HOME\/} ;; ##################################### @@ -116,8 +114,11 @@ while [ -n "$1" ]; do shift done -# replace '~' by $HOME: +# Check the input argument of the install path and (if used) replace the tilde +# character '~' by the users home directory ${HOME}. Afterwards clear the +# PREFIX input variable. PREFIX_PATH=${PREFIX/#~\//$HOME\/} +unset PREFIX RE='^[0-9]+$' if [[ ! "${JOBS}" =~ ${RE} || ${JOBS}<1 ]] ; then