tuned messages;
authorwenzelm
Mon, 13 Jan 2020 12:11:25 +0100
changeset 71375 5ccf60c1f47c
parent 71374 7832d912d950
child 71376 26801434d628
tuned messages;
src/Pure/build-jars
src/Tools/jEdit/lib/Tools/jedit
--- 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 ..."
 
--- 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 ..."