diff -r c347986773eb -r 9a7f17370ffb lib/scripts/getsettings --- 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