lib/Tools/java
changeset 47986 1a05adae1cc9
parent 47984 b5a5662528fb
child 48336 71d5f37ee2bf
     1.1 --- a/lib/Tools/java	Mon Mar 26 15:38:09 2012 +0200
     1.2 +++ b/lib/Tools/java	Mon Mar 26 16:25:08 2012 +0200
     1.3 @@ -6,21 +6,12 @@
     1.4  
     1.5  CLASSPATH="$(jvmpath "$CLASSPATH")"
     1.6  
     1.7 -JAVA_EXE="$ISABELLE_JDK_HOME/bin/java"
     1.8 -
     1.9 -if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
    1.10 -  :
    1.11 -else
    1.12 -  echo "Bad Java executable: \"$JAVA_EXE\"" >&2
    1.13 -  exit 2
    1.14 -fi
    1.15 -
    1.16 -if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
    1.17 +if isabelle_jdk java -server >/dev/null 2>/dev/null; then
    1.18    SERVER="-server"
    1.19  else
    1.20    SERVER=""
    1.21  fi
    1.22  
    1.23 -exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
    1.24 +exec "$ISABELLE_JDK_HOME/bin/java" -Dfile.encoding=UTF-8 $SERVER \
    1.25    "-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
    1.26