lib/Tools/java_monitor
changeset 72978 7e7ed27fe625
parent 72976 51442c6dc296
child 72981 c78d1dfc6571
equal deleted inserted replaced
72977:e028331c578b 72978:7e7ed27fe625
     2 #
     2 #
     3 # Author: Makarius
     3 # Author: Makarius
     4 #
     4 #
     5 # DESCRIPTION: monitor another Java process
     5 # DESCRIPTION: monitor another Java process
     6 
     6 
     7 isabelle_admin_build jars || exit $?
       
     8 
       
     9 isabelle java isabelle.Java_Monitor "$@"
     7 isabelle java isabelle.Java_Monitor "$@"