Wed, 26 Feb 2020 14:47:36 +0100 | wenzelm | obsolete; | file | diff | annotate |
Wed, 26 Feb 2020 14:43:43 +0100 | wenzelm | proper message passing -- discontinued obsolete auxiliary commands; | file | diff | annotate |
Tue, 25 Feb 2020 21:28:06 +0100 | wenzelm | clarified Panel; | file | diff | annotate |
Tue, 25 Feb 2020 18:30:08 +0100 | wenzelm | update to WebviewPanel API, following initial version by Peter Zeller; | file | diff | annotate |
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 |