| Fri, 11 Aug 2017 18:08:46 +0200 | wenzelm | proper state_panel exit; | file | diff | annotate |
| Thu, 29 Jun 2017 11:36:25 +0200 | wenzelm | HTML GUI actions via JavaScript; | file | diff | annotate |
| Tue, 27 Jun 2017 16:50:40 +0200 | wenzelm | added missing files (cf. 5aa9cb83e70e); | file | diff | annotate |