| Tue, 22 Apr 2014 12:41:34 +0200 | wenzelm | favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables; | changeset | files |
| Tue, 22 Apr 2014 12:30:54 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 22 Apr 2014 12:05:02 +0200 | wenzelm | clarified exit code for the rare situation where Runtime.exn_error_message might fail; | changeset | files |