changeset 53970 | eee1863c565a |
parent 53967 | bfaae48b0ce0 |
child 56439 | 95e2656b3b23 |
53969:7ed81754b069 | 53970:eee1863c565a |
---|---|
17 fi |
17 fi |
18 |
18 |
19 #Cygwin vs. POSIX |
19 #Cygwin vs. POSIX |
20 if [ "$OSTYPE" = cygwin ] |
20 if [ "$OSTYPE" = cygwin ] |
21 then |
21 then |
22 unset INI_DIR |
|
23 |
|
22 if [ -z "$USER_HOME" ]; then |
24 if [ -z "$USER_HOME" ]; then |
23 USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")" |
25 USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")" |
24 fi |
26 fi |
25 |
27 |
26 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |
28 function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; } |