# HG changeset patch
# User wenzelm
# Date 1578913768 -3600
# Node ID 7832d912d950b658744e7d87ed8ef473dea42b4f
# Parent  201486ced92d0fd9685338ade9f36d97f4dedb2f
tuned;

diff -r 201486ced92d -r 7832d912d950 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