tuned;
authorwenzelm
Mon, 13 Jan 2020 12:09:28 +0100
changeset 71374 7832d912d950
parent 71373 201486ced92d
child 71375 5ccf60c1f47c
tuned;
src/Pure/build-jars
--- 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