equal
deleted
inserted
replaced
63 echo "### Building graph browser ..." |
63 echo "### Building graph browser ..." |
64 echo "###" |
64 echo "###" |
65 |
65 |
66 rm -rf classes && mkdir classes |
66 rm -rf classes && mkdir classes |
67 |
67 |
68 "$ISABELLE_JDK_HOME/bin/javac" -d classes -source 1.4 "${SOURCES[@]}" || \ |
68 isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \ |
69 fail "Failed to compile sources" |
69 fail "Failed to compile sources" |
70 "$ISABELLE_JDK_HOME/bin/jar" cf "$(jvmpath "$TARGET")" -C classes . || |
70 isabelle_jdk jar cf "$(jvmpath "$TARGET")" -C classes . || |
71 fail "Failed to produce $TARGET" |
71 fail "Failed to produce $TARGET" |
72 |
72 |
73 rm -rf classes |
73 rm -rf classes |
74 fi |
74 fi |