equal
deleted
inserted
replaced
5 # DESCRIPTION: invoke Java within the Isabelle environment |
5 # DESCRIPTION: invoke Java within the Isabelle environment |
6 |
6 |
7 CLASSPATH="$(jvmpath "$CLASSPATH")" |
7 CLASSPATH="$(jvmpath "$CLASSPATH")" |
8 |
8 |
9 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
9 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
10 if "$JAVA_EXE" -server >/dev/null 2>/dev/null |
10 |
11 then |
11 if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then |
12 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 -server "$@" |
12 SERVER="-server" |
13 else |
13 else |
14 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 "$@" |
14 SERVER="" |
15 fi |
15 fi |
16 |
16 |
|
17 exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \ |
|
18 "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@" |
|
19 |