| Thu, 27 Aug 2020 12:34:10 +0200 | wenzelm | clarified signature; | file | diff | annotate |
| Sat, 15 Aug 2020 13:45:25 +0200 | wenzelm | clarified names; | file | diff | annotate |
| Thu, 13 Aug 2020 15:11:30 +0200 | wenzelm | support JVM runtime statistics; | file | diff | annotate |
| Thu, 13 Aug 2020 12:38:44 +0200 | wenzelm | clarified order for GUI; | file | diff | annotate |
| Wed, 12 Aug 2020 19:32:45 +0200 | wenzelm | support for Poly/ML memory status; | file | diff | annotate |
| Wed, 12 Aug 2020 11:26:01 +0200 | wenzelm | removed pointless option "ML_statistics": always enabled; | file | diff | annotate |
| Fri, 07 Aug 2020 22:57:14 +0200 | wenzelm | provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored); | file | diff | annotate |