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