lib/Tools/java_monitor
changeset 72981 c78d1dfc6571
parent 72978 7e7ed27fe625
child 74360 9e71155e3666
equal deleted inserted replaced
72978:7e7ed27fe625 72981:c78d1dfc6571
     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 java isabelle.Java_Monitor "$@"
     7 isabelle java "-Dapple.awt.application.name=Java Monitor" isabelle.Java_Monitor "$@"