| changeset 71375 | 5ccf60c1f47c |
| parent 71372 | 85274743f789 |
| child 71548 | e32255318cb2 |
--- 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 ..."