diff options
| -rwxr-xr-x | tools/configure | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/configure b/tools/configure index 209ef4c..7c61b09 100755 --- a/tools/configure +++ b/tools/configure @@ -3092,7 +3092,7 @@ if [ "$ARG_RBDIR" ]; then if [ "$need_full_path" = "yes" ]; then rbdir=`realpath $ARG_RBDIR` else # prepend '/' if needed - if [ -z `echo $ARG_RBDIR | grep -P '/.*'` ]; then + if [ -z `echo $ARG_RBDIR | grep '^/'` ]; then rbdir="/"$ARG_RBDIR else rbdir=$ARG_RBDIR |