# HG changeset patch
# User wenzelm
# Date 1608589334 -3600
# Node ID 7e7ed27fe62572eb43c427bd2242119714b33aa4
# Parent  e028331c578b5bca7e48de85db66d36f30b24103
less aggressive auto-build: avoid change of running jar;

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 "$@"