# HG changeset patch # User wenzelm # Date 1434809327 -7200 # Node ID 9cc91b8a6489c0617f52c2bdc7d45b250dedc4b9 # Parent 44f9873d6f6f24885d868c1d01e246e8b7139ec4 less ambitious USER_HOME on Windows: avoid potentially disconnected share, agree with guess of JVM user.home; diff -r 44f9873d6f6f -r 9cc91b8a6489 lib/scripts/getsettings --- a/lib/scripts/getsettings Sat Jun 20 15:45:02 2015 +0200 +++ b/lib/scripts/getsettings Sat Jun 20 16:08:47 2015 +0200 @@ -33,7 +33,7 @@ fi if [ -z "$USER_HOME" ]; then - USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")" + USER_HOME="$(cygpath -u "$USERPROFILE")" fi function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }