| author | wenzelm |
| Mon, 07 Nov 2011 14:59:58 +0100 | |
| changeset 45385 | 7c1375ba1424 |
| parent 43536 | lib/scripts/java_ext_dirs@6eec653d5599 |
| child 47113 | b5a5662528fb |
| permissions | -rwxr-xr-x |
| 43518 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# Author: Makarius |
|
4 |
# |
|
5 |
# Augment Java extension directories. |
|
6 |
||
7 |
## diagnostics |
|
8 |
||
9 |
function fail() |
|
10 |
{
|
|
11 |
echo "$1" >&2 |
|
12 |
exit 2 |
|
13 |
} |
|
14 |
||
|
45385
7c1375ba1424
offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
43536
diff
changeset
|
15 |
[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment" |
| 43518 | 16 |
|
17 |
||
18 |
## main |
|
19 |
||
20 |
JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
|
|
|
45385
7c1375ba1424
offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
43536
diff
changeset
|
21 |
exec "$JAVA_EXE" -classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \ |
|
7c1375ba1424
offline build of java_ext_dirs.jar, to avoid runtime dependency on javac/jar executables;
wenzelm
parents:
43536
diff
changeset
|
22 |
isabelle.Java_Ext_Dirs "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" |
| 43518 | 23 |