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