Fri, 11 Aug 2017 19:09:42 +0200 | wenzelm | avoid spurious output after exit; | file | diff | annotate |
Thu, 29 Jun 2017 11:58:00 +0200 | wenzelm | proper dynamic controls, notably for auto_update_enabled; | file | diff | annotate |
Thu, 29 Jun 2017 11:42:42 +0200 | wenzelm | tuned signature; | file | diff | annotate |
Thu, 29 Jun 2017 11:36:25 +0200 | wenzelm | HTML GUI actions via JavaScript; | file | diff | annotate |
Tue, 27 Jun 2017 21:56:56 +0200 | wenzelm | clarified defaults; | file | diff | annotate |
Tue, 27 Jun 2017 11:49:47 +0200 | wenzelm | GUI controls similar to Tools/jEdit/src/state_dockable.scala; | file | diff | annotate |
Fri, 16 Jun 2017 22:38:19 +0200 | wenzelm | tuned; | file | diff | annotate |
Fri, 16 Jun 2017 21:04:39 +0200 | wenzelm | clarified modules; | file | diff | annotate | base |