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 |