diff options
Diffstat (limited to 'tools/configure')
-rwxr-xr-x | tools/configure | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/configure b/tools/configure index 209ef4c746..7c61b09ee7 100755 --- a/tools/configure +++ b/tools/configure | |||
@@ -3092,7 +3092,7 @@ if [ "$ARG_RBDIR" ]; then | |||
3092 | if [ "$need_full_path" = "yes" ]; then | 3092 | if [ "$need_full_path" = "yes" ]; then |
3093 | rbdir=`realpath $ARG_RBDIR` | 3093 | rbdir=`realpath $ARG_RBDIR` |
3094 | else # prepend '/' if needed | 3094 | else # prepend '/' if needed |
3095 | if [ -z `echo $ARG_RBDIR | grep -P '/.*'` ]; then | 3095 | if [ -z `echo $ARG_RBDIR | grep '^/'` ]; then |
3096 | rbdir="/"$ARG_RBDIR | 3096 | rbdir="/"$ARG_RBDIR |
3097 | else | 3097 | else |
3098 | rbdir=$ARG_RBDIR | 3098 | rbdir=$ARG_RBDIR |