--- a/lib/scripts/getsettings Thu Aug 28 22:09:20 2008 +0200
+++ b/lib/scripts/getsettings Thu Aug 28 22:26:21 2008 +0200
@@ -53,6 +53,7 @@
function jvmpath() { echo "$@"; }
ISABELLE_ROOT_JVM=/
fi
+HOME_JVM="$HOME"
#CLASSPATH convenience
function classpath () {