1.1 --- a/lib/scripts/getsettings Thu Aug 21 16:02:54 2008 +0200
1.2 +++ b/lib/scripts/getsettings Thu Aug 21 17:42:59 2008 +0200
1.3 @@ -48,10 +48,10 @@
1.4 if [ "$OSTYPE" = cygwin ]; then
1.5 CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
1.6 function jvmpath() { cygpath -w -p "$@"; }
1.7 - ISABELLE_ROOT_JVM="/"
1.8 + ISABELLE_ROOT_JVM="$(jvmpath /)"
1.9 else
1.10 function jvmpath() { echo "$@"; }
1.11 - ISABELLE_ROOT_JVM="$(jvmpath "/")"
1.12 + ISABELLE_ROOT_JVM=/
1.13 fi
1.14
1.15 #CLASSPATH convenience