diff -r e028331c578b -r 7e7ed27fe625 lib/Tools/java_monitor --- a/lib/Tools/java_monitor Mon Dec 21 22:55:57 2020 +0100 +++ b/lib/Tools/java_monitor Mon Dec 21 23:22:14 2020 +0100 @@ -4,6 +4,4 @@ # # DESCRIPTION: monitor another Java process -isabelle_admin_build jars || exit $? - isabelle java isabelle.Java_Monitor "$@"