equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # Author: Makarius |
4 # Author: Makarius |
5 # |
5 # |
6 # DESCRIPTION: Java wrapper |
6 # DESCRIPTION: invoke Java within the Isabelle environment |
7 |
|
8 |
|
9 PRG="$(basename "$0")" |
|
10 |
|
11 function usage() |
|
12 { |
|
13 echo |
|
14 echo "Usage: $PRG [ARGS ...]" |
|
15 echo |
|
16 echo " Invoke Java within the Isabelle environment." |
|
17 echo |
|
18 exit 1 |
|
19 } |
|
20 |
|
21 |
|
22 ## main |
|
23 |
7 |
24 CLASSPATH="$(jvmpath "$CLASSPATH")" |
8 CLASSPATH="$(jvmpath "$CLASSPATH")" |
25 exec "$ISABELLE_JAVA" "$@" |
9 exec "$ISABELLE_JAVA" "$@" |