| Sat, 07 Mar 2020 12:19:41 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 07 Mar 2020 12:15:15 +0100 | wenzelm | copy jEdit sources instead of jar, for better browsing experience; | changeset | files |
| Sat, 07 Mar 2020 12:14:51 +0100 | wenzelm | proper option; | changeset | files |