# HG changeset patch
# User wenzelm
# Date 1578913885 -3600
# Node ID 5ccf60c1f47c7c22a3284b1cbc4cec45a8d23e5a
# Parent  7832d912d950b658744e7d87ed8ef473dea42b4f
tuned messages;

diff -r 7832d912d950 -r 5ccf60c1f47c src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Jan 13 12:09:28 2020 +0100
+++ b/src/Pure/build-jars	Mon Jan 13 12:11:25 2020 +0100
@@ -273,7 +273,7 @@
 
 ## build
 
-target_shasum | cmp "$TARGET_SHASUM" 2>/dev/null
+target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
 if [ "$?" -ne 0 ]; then
   echo "### Building Isabelle/Scala ..."
 
diff -r 7832d912d950 -r 5ccf60c1f47c src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Jan 13 12:09:28 2020 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Jan 13 12:11:25 2020 +0100
@@ -331,7 +331,7 @@
   rm -rf "$ISABELLE_HOME/$BUILD_DIR"
 }
 
-target_shasum | cmp "$TARGET_SHASUM" 2>/dev/null
+target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
 if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
   echo "### Building Isabelle/jEdit ..."