diff --git a/configure/tools/fullPathName.pl b/configure/tools/fullPathName.pl index a194c6f69..3e8e60901 100755 --- a/configure/tools/fullPathName.pl +++ b/configure/tools/fullPathName.pl @@ -12,6 +12,7 @@ if( $ARGV[0] ) { if( $ARGV[0] =~ /^\./ ) { $dir = abs_path("$ARGV[0]"); + $dir =~ s/\/tmp_mnt//; print "$dir\n"; } else { print "$ARGV[0]\n";