diff -r 00ede188c5d6 -r 0a99c8716312 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Mon Jun 08 20:43:57 2009 +0200
+++ b/lib/scripts/getsettings	Tue Jun 09 01:32:57 2009 +0200
@@ -51,10 +51,8 @@
 if [ "$OSTYPE" = cygwin ]; then
   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
   function jvmpath() { cygpath -w -p "$@"; }
-  ISABELLE_ROOT_JVM="$(jvmpath /)"
 else
   function jvmpath() { echo "$@"; }
-  ISABELLE_ROOT_JVM=/
 fi
 HOME_JVM="$HOME"