lib/scripts/getsettings
changeset 47661 012a887997f3
parent 47525 9c8a1b9c0630
child 47748 24550210de0b
     1.1 --- a/lib/scripts/getsettings	Sun Apr 22 11:05:04 2012 +0200
     1.2 +++ b/lib/scripts/getsettings	Sun Apr 22 14:30:18 2012 +0200
     1.3 @@ -11,9 +11,13 @@
     1.4  
     1.5  ISABELLE_SETTINGS_PRESENT=true
     1.6  
     1.7 -#JVM path wrapper
     1.8 +#Cygwin vs Posix
     1.9  if [ "$OSTYPE" = cygwin ]
    1.10  then
    1.11 +  if [ -z "$USER_HOME" ]; then
    1.12 +    USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
    1.13 +  fi
    1.14 +
    1.15    ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
    1.16    ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
    1.17  
    1.18 @@ -21,10 +25,13 @@
    1.19    function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
    1.20    THIS_CYGWIN="$(jvmpath "/")"
    1.21  else
    1.22 +  if [ -z "$USER_HOME" ]; then
    1.23 +    USER_HOME="$HOME"
    1.24 +  fi
    1.25 +
    1.26    function jvmpath() { echo "$@"; }
    1.27    CLASSPATH="$CLASSPATH"
    1.28  fi
    1.29 -HOME_JVM="$HOME"
    1.30  
    1.31  export ISABELLE_HOME
    1.32  if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }