| Mon, 18 Sep 2017 10:32:09 +0200 | wenzelm | store document version; | changeset | files |
| Mon, 18 Sep 2017 10:28:22 +0200 | wenzelm | auto update; | changeset | files |
| 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 |
| Sat, 16 Sep 2017 15:35:56 +0200 | wenzelm | proper standard_path to revert platform_path in JEdit_Sessions.session_base; | changeset | files |