| changeset 36238 | 344377ce2e0a |
| parent 36212 | ebfa4bb0d50f |
| child 41380 | 92237dee0f29 |
| 36237:86e62a98deea | 36238:344377ce2e0a |
|---|---|
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 exec "${THIS_JAVA:-$ISABELLE_JAVA}" "$@" |