equal
deleted
inserted
replaced
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 |
|
15 |
|
16 ## dependencies |
|
17 |
|
18 SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java" |
|
19 |
|
20 TARGET_DIR="$ISABELLE_HOME/lib/classes" |
|
21 TARGET="$TARGET_DIR/java_ext_dirs.jar" |
|
22 |
|
23 if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then |
|
24 mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\"" |
|
25 pushd "$TARGET_DIR" >/dev/null |
|
26 |
|
27 BUILD="build$$" |
|
28 TMP_JAR="java_ext_dirs$$.jar" |
|
29 |
|
30 rm -rf "$BUILD" && mkdir "$BUILD" |
|
31 javac -d "$BUILD" -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources" |
|
32 jar cf "$TMP_JAR" -C "$BUILD" . || fail "Failed to produce $TMP_JAR" |
|
33 mv "$TMP_JAR" "$TARGET" |
|
34 rm -rf "$BUILD" |
|
35 |
|
36 popd >/dev/null |
|
37 fi |
|
38 |
|
39 |
|
40 ## main |
|
41 |
|
42 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}" |
|
43 exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \ |
|
44 "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")" |
|
45 |
|