author | wenzelm |
Mon, 13 Jan 2020 12:09:28 +0100 | |
changeset 71374 | 7832d912d950 |
parent 71373 | 201486ced92d |
child 71375 | 5ccf60c1f47c |
--- a/src/Pure/build-jars Mon Jan 13 11:19:24 2020 +0100 +++ b/src/Pure/build-jars Mon Jan 13 12:09:28 2020 +0100 @@ -258,16 +258,16 @@ TARGET_JAR="$TARGET_DIR/Pure.jar" TARGET_SHASUM="$TARGET_DIR/Pure.shasum" +function target_shasum() +{ + shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null +} + function target_clean() { rm -rf "$TARGET_DIR" } -function target_shasum() -{ - shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null -} - [ -n "$FRESH" ] && target_clean