equal
deleted
inserted
replaced
63 [ "$#" -ne 0 ] && usage |
63 [ "$#" -ne 0 ] && usage |
64 |
64 |
65 |
65 |
66 ## main |
66 ## main |
67 |
67 |
68 isabelle_admin_build jars || exit $? |
68 isabelle_scala_build || exit $? |
69 |
69 |
70 if [ -n "$GRAPHFILE" ]; then |
70 if [ -n "$GRAPHFILE" ]; then |
71 PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE") |
71 PRIVATE_FILE="${ISABELLE_TMP:-${TMPDIR:-/tmp}}/$$"$(basename "$GRAPHFILE") |
72 if [ -n "$CLEAN" ]; then |
72 if [ -n "$CLEAN" ]; then |
73 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE" |
73 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE" |