changeset 64223 | 9d5b9f41df77 |
parent 64200 | 2e6597279d38 |
child 73705 | ac07f6be27ea |
--- a/Admin/build_history Sat Oct 15 14:15:29 2016 +0200 +++ b/Admin/build_history Sat Oct 15 15:14:46 2016 +0200 @@ -4,5 +4,5 @@ THIS="$(cd "$(dirname "$0")"; pwd)" -"$THIS/build" jars || exit $? +"$THIS/build" jars > /dev/null || exit $? exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"