lib/Tools/java_monitor
changeset 72976 51442c6dc296
child 72978 7e7ed27fe625
equal deleted inserted replaced
72975:315f9b4f9e7a 72976:51442c6dc296
       
     1 #!/usr/bin/env bash
       
     2 #
       
     3 # Author: Makarius
       
     4 #
       
     5 # DESCRIPTION: monitor another Java process
       
     6 
       
     7 isabelle_admin_build jars || exit $?
       
     8 
       
     9 isabelle java isabelle.Java_Monitor "$@"