lib/Tools/java_monitor
author wenzelm
Wed, 31 Mar 2021 11:24:46 +0200
changeset 73772 d3f2038198ae
parent 73222 c78d1dfc6571
child 74726 9e71155e3666
permissions -rwxr-xr-x
clarified (again): local tip could be actually more recent;

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: monitor another Java process

isabelle java "-Dapple.awt.application.name=Java Monitor" isabelle.Java_Monitor "$@"