Tue, 13 Jun 2017 11:53:24 +0200 | wenzelm | updated package; | changeset | files |
Tue, 13 Jun 2017 11:34:05 +0200 | wenzelm | tuned GUI; | changeset | files |
Tue, 13 Jun 2017 11:13:34 +0200 | wenzelm | obsolete; | changeset | files |
Mon, 12 Jun 2017 21:14:38 +0200 | wenzelm | removed pointless entries: not part of api.LanguageEntry; | changeset | files |
Mon, 12 Jun 2017 21:12:59 +0200 | wenzelm | avoid overlapping line background, notably for "quoted"; | changeset | files |
Mon, 12 Jun 2017 20:24:40 +0200 | wenzelm | tuned rendering; | changeset | files |
Mon, 12 Jun 2017 20:06:55 +0200 | wenzelm | tuned; | changeset | files |