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 "### Building graph browser ..." |
62 echo >&2 "### 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.6 "${SOURCES[@]}" || \ |
66 isabelle_jdk javac -d classes -source 1.6 "${SOURCES[@]}" || \ |
67 fail "Failed to compile sources" |
67 fail "Failed to compile sources" |