equal
deleted
inserted
replaced
57 [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true |
57 [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true |
58 done |
58 done |
59 |
59 |
60 if [ "$OUTDATED" = true ] |
60 if [ "$OUTDATED" = true ] |
61 then |
61 then |
62 echo "###" |
|
63 echo "### Building graph browser ..." |
62 echo "### Building graph browser ..." |
64 echo "###" |
|
65 |
63 |
66 rm -rf classes && mkdir classes |
64 rm -rf classes && mkdir classes |
67 |
65 |
68 isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \ |
66 isabelle_jdk javac -d classes -source 1.4 "${SOURCES[@]}" || \ |
69 fail "Failed to compile sources" |
67 fail "Failed to compile sources" |