| Thu, 29 Jun 2017 21:27:34 +0200 | wenzelm | updated package; | changeset | files |
| Thu, 29 Jun 2017 21:09:39 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 29 Jun 2017 21:07:47 +0200 | wenzelm | tuned output; | changeset | files |
| Thu, 29 Jun 2017 20:59:49 +0200 | wenzelm | tuned spelling; | changeset | files |
| Thu, 29 Jun 2017 17:37:57 +0200 | wenzelm | more documentation; | changeset | files |
| Thu, 29 Jun 2017 17:37:03 +0200 | wenzelm | auto update; | changeset | files |
| Thu, 29 Jun 2017 15:12:40 +0200 | wenzelm | clarified editor focus; | changeset | files |
| Thu, 29 Jun 2017 14:39:24 +0200 | wenzelm | proper hyperlink_command, notably for locate_query; | changeset | files |
| Thu, 29 Jun 2017 13:28:08 +0200 | wenzelm | tuned signature; | changeset | files |
| Thu, 29 Jun 2017 11:58:00 +0200 | wenzelm | proper dynamic controls, notably for auto_update_enabled; | changeset | files |
| Thu, 29 Jun 2017 11:42:42 +0200 | wenzelm | tuned signature; | changeset | files |
| Thu, 29 Jun 2017 11:36:25 +0200 | wenzelm | HTML GUI actions via JavaScript; | changeset | files |