| Sun, 17 Sep 2017 21:46:17 +0200 | wenzelm | updated imports; | changeset | files |
| Sun, 17 Sep 2017 17:37:40 +0200 | wenzelm | more documentation; | changeset | files |
| Sat, 16 Sep 2017 17:25:51 +0200 | wenzelm | more derived actions, according to jEdit/org/gjt/sp/jedit/gui/DockableWindowFactory.java; | changeset | files |
| Sat, 16 Sep 2017 16:19:34 +0200 | wenzelm | proper tool name (cf. c1410bcf6e87); | changeset | files |