lib/scripts/getsettings

--- a/lib/scripts/getsettings	Thu Aug 21 16:02:54 2008 +0200
+++ b/lib/scripts/getsettings	Thu Aug 21 17:42:59 2008 +0200
@@ -48,10 +48,10 @@
 if [ "$OSTYPE" = cygwin ]; then
   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
   function jvmpath() { cygpath -w -p "$@"; }
-  ISABELLE_ROOT_JVM="/"
+  ISABELLE_ROOT_JVM="$(jvmpath /)"
 else
   function jvmpath() { echo "$@"; }
-  ISABELLE_ROOT_JVM="$(jvmpath "/")"
+  ISABELLE_ROOT_JVM=/
 fi
 
 #CLASSPATH convenience