| author | wenzelm |
| Mon, 07 Nov 2011 14:59:58 +0100 | |
| changeset 46258 | 7c1375ba1424 |
| parent 45990 | 21c09b727bf3 |
| child 47984 | b5a5662528fb |
| 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@46258 | 25 |
"-Djava.ext.dirs=$("$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs")" "$@"
|
| wenzelm@44401 | 26 |