author | wenzelm |
Sat, 07 Aug 2021 19:29:41 +0200 | |
changeset 74139 | 3314559ef095 |
parent 72981 | c78d1dfc6571 |
child 74360 | 9e71155e3666 |
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 |
|
72981 | 7 |
isabelle java "-Dapple.awt.application.name=Java Monitor" isabelle.Java_Monitor "$@" |