--- 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 ..."