equal
deleted
inserted
replaced
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
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 exec "${THIS_JAVA:-$ISABELLE_JAVA}" "$@" |
8 |
|
9 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
|
10 if "$JAVA_EXE" -server >/dev/null 2>/dev/null |
|
11 then |
|
12 exec "$JAVA_EXE" -server "$@" |
|
13 else |
|
14 exec "$JAVA_EXE" "$@" |
|
15 fi |
|
16 |