diff -r 315f9b4f9e7a -r 51442c6dc296 lib/Tools/java_monitor
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/java_monitor	Mon Dec 21 22:47:53 2020 +0100
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: monitor another Java process
+
+isabelle_admin_build jars || exit $?
+
+isabelle java isabelle.Java_Monitor "$@"