| 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 |
| Sat, 16 Sep 2017 15:35:56 +0200 | wenzelm | proper standard_path to revert platform_path in JEdit_Sessions.session_base; | changeset | files |