Thu, 13 Aug 2020 12:38:44 +0200 | wenzelm | clarified order for GUI; | changeset | files |
Thu, 13 Aug 2020 12:33:44 +0200 | wenzelm | tuned; | changeset | files |
Thu, 13 Aug 2020 12:29:39 +0200 | wenzelm | clarified GUI; | changeset | files |
Wed, 12 Aug 2020 20:09:37 +0200 | wenzelm | show GC progress as "ML cleanup"; | changeset | files |
Wed, 12 Aug 2020 19:34:38 +0200 | wenzelm | ML status widget similar to org.gjt.sp.jedit.gui.statusbar.MemoryStatusWidgetFactory; | changeset | files |
Wed, 12 Aug 2020 19:32:45 +0200 | wenzelm | support for Poly/ML memory status; | changeset | files |