lib/scripts/getsettings
changeset 27914 9a7f17370ffb
parent 27911 31523791345a
child 27934 7d12a7e3cc55
--- a/lib/scripts/getsettings	Sat Aug 16 13:31:56 2008 +0200
+++ b/lib/scripts/getsettings	Sat Aug 16 13:31:57 2008 +0200
@@ -44,18 +44,13 @@
   echo "$RESULT"
 }
 
-#JVM path wrappers
+#JVM path wrapper
 if [ "$OSTYPE" = cygwin ]; then
   CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
   function jvmpath() { cygpath -w -p "$@"; }
-  function javawrapper() { env CLASSPATH="$(jvmpath "$CLASSPATH")" java "$@"; }
-  function scalawrapper() { env CLASSPATH="$(jvmpath "$CLASSPATH")" scala "$@"; }
 else
   function jvmpath() { echo "$@"; }
-  function javawrapper() { java "$@"; }
-  function scalawrapper() { scala "$@"; }
 fi
-ISABELLE_HOME_JVM="$(jvmpath "$ISABELLE_HOME")"
 
 #CLASSPATH convenience
 function classpath () {
@@ -87,6 +82,10 @@
 
 ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
 
+#JVM settings
+ISABELLE_HOME_JVM="$(jvmpath "$ISABELLE_HOME")"
+ISABELLE_HOME_USER_JVM="$(jvmpath "$ISABELLE_HOME_USER")"
+
 set +o allexport
 
 fi