author | wenzelm |
Tue, 04 Oct 2011 14:51:51 +0200 | |
changeset 45990 | 21c09b727bf3 |
parent 44401 | d477b92109b8 |
child 46258 | 7c1375ba1424 |
permissions | -rwxr-xr-x |
wenzelm@27914 | 1 |
#!/usr/bin/env bash |
wenzelm@27914 | 2 |
# |
wenzelm@27914 | 3 |
# Author: Makarius |
wenzelm@27914 | 4 |
# |
wenzelm@27916 | 5 |
# DESCRIPTION: invoke Java within the Isabelle environment |
wenzelm@27914 | 6 |
|
wenzelm@27914 | 7 |
CLASSPATH="$(jvmpath "$CLASSPATH")" |
wenzelm@41629 | 8 |
|
wenzelm@41629 | 9 |
JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
wenzelm@44401 | 10 |
|
wenzelm@45990 | 11 |
if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then |
wenzelm@45990 | 12 |
: |
wenzelm@45990 | 13 |
else |
wenzelm@45990 | 14 |
echo "Bad Java executable: \"$JAVA_EXE\"" >&2 |
wenzelm@45990 | 15 |
exit 2 |
wenzelm@45990 | 16 |
fi |
wenzelm@45990 | 17 |
|
wenzelm@44401 | 18 |
if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then |
wenzelm@44401 | 19 |
SERVER="-server" |
wenzelm@41629 | 20 |
else |
wenzelm@44401 | 21 |
SERVER="" |
wenzelm@41629 | 22 |
fi |
wenzelm@41629 | 23 |
|
wenzelm@44401 | 24 |
exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \ |
wenzelm@44401 | 25 |
"-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@" |
wenzelm@44401 | 26 |