--- 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 () {