changeset 72978 | 7e7ed27fe625 |
parent 72976 | 51442c6dc296 |
child 72981 | c78d1dfc6571 |
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 "$@" |