# HG changeset patch
# User wenzelm
# Date 1218835897 -7200
# Node ID 31523791345a70ee61ae3cf826fc7c9494987cc6
# Parent  6f60110e317cc605b6fbe8e9d296578800c087e4
added ISABELLE_HOME_JVM;

diff -r 6f60110e317c -r 31523791345a lib/scripts/getsettings
--- a/lib/scripts/getsettings	Fri Aug 15 23:10:36 2008 +0200
+++ b/lib/scripts/getsettings	Fri Aug 15 23:31:37 2008 +0200
@@ -55,6 +55,7 @@
   function javawrapper() { java "$@"; }
   function scalawrapper() { scala "$@"; }
 fi
+ISABELLE_HOME_JVM="$(jvmpath "$ISABELLE_HOME")"
 
 #CLASSPATH convenience
 function classpath () {