equal
deleted
inserted
replaced
329 { |
329 { |
330 isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed |
330 isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed |
331 rm -rf "$ISABELLE_HOME/$BUILD_DIR" |
331 rm -rf "$ISABELLE_HOME/$BUILD_DIR" |
332 } |
332 } |
333 |
333 |
334 target_shasum | cmp "$TARGET_SHASUM" 2>/dev/null |
334 target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null |
335 if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then |
335 if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then |
336 echo "### Building Isabelle/jEdit ..." |
336 echo "### Building Isabelle/jEdit ..." |
337 |
337 |
338 [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ |
338 [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ |
339 fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" |
339 fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" |