author | wenzelm |
Mon, 21 Dec 2020 23:22:14 +0100 | |
changeset 72978 | 7e7ed27fe625 |
parent 72976 | 51442c6dc296 |
child 72981 | c78d1dfc6571 |
permissions | -rwxr-xr-x |
72976
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
1 |
#!/usr/bin/env bash |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
2 |
# |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
3 |
# Author: Makarius |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
4 |
# |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
5 |
# DESCRIPTION: monitor another Java process |
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
6 |
|
51442c6dc296
more robust Java monitor: avoid odd warning about insecure connection;
wenzelm
parents:
diff
changeset
|
7 |
isabelle java isabelle.Java_Monitor "$@" |