author | wenzelm |
Mon, 26 Mar 2012 16:25:08 +0200 | |
changeset 47115 | 1a05adae1cc9 |
parent 47113 | b5a5662528fb |
child 47465 | 71d5f37ee2bf |
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 |
||
47115
1a05adae1cc9
more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);
wenzelm
parents:
47113
diff
changeset
|
20 |
isabelle_jdk java \ |
47113
b5a5662528fb
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents:
45385
diff
changeset
|
21 |
-classpath "$(jvmpath "$ISABELLE_HOME/src/Tools/JVM/java_ext_dirs.jar")" \ |
45385
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 |