stan/jdk-24
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

8303427: Fixpath confused if unix root contains "/jdk"

Browse Source 
Reviewed-by: mikael
This commit is contained in:
Erik Joelsson 2023-09-01 17:12:56 +00:00
parent e9e0c5699b
commit 2f7c65ec48
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
make/scripts/fixpath.sh
View File

@ -326,7 +326,9 @@ function convert_path() {
suffix="${BASH_REMATCH[6]}" suffix="${BASH_REMATCH[6]}"
# We only believe this is a path if the first part is an existing directory # We only believe this is a path if the first part is an existing directory
if [[ -d "/$firstdir" ]]; then # and the prefix is not a subdirectory in the current working directory. Remove
# any part leading up to a : or = in the prefix before checking.
if [[ -d "/$firstdir" && ! -d "${prefix##*:}" && ! -d "${prefix##*=}" ]]; then
if [[ $ENVROOT == "" ]]; then if [[ $ENVROOT == "" ]]; then
if [[ $QUIET != true ]]; then if [[ $QUIET != true ]]; then
echo fixpath: failure: Path "'"$pathmatch"'" cannot be converted to Windows path >&2 echo fixpath: failure: Path "'"$pathmatch"'" cannot be converted to Windows path >&2