diff -r 7c9e31ffcd9e -r 1a05adae1cc9 lib/Tools/java --- a/lib/Tools/java Mon Mar 26 15:38:09 2012 +0200 +++ b/lib/Tools/java Mon Mar 26 16:25:08 2012 +0200 @@ -6,21 +6,12 @@ CLASSPATH="$(jvmpath "$CLASSPATH")" -JAVA_EXE="$ISABELLE_JDK_HOME/bin/java" - -if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then - : -else - echo "Bad Java executable: \"$JAVA_EXE\"" >&2 - exit 2 -fi - -if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then +if isabelle_jdk java -server >/dev/null 2>/dev/null; then SERVER="-server" else SERVER="" fi -exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \ +exec "$ISABELLE_JDK_HOME/bin/java" -Dfile.encoding=UTF-8 $SERVER \ "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"