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 |
Fri, 06 Mar 2020 22:01:28 +0100 | wenzelm | tuned; | changeset | files |
Fri, 06 Mar 2020 20:33:16 +0100 | wenzelm | formally depend on Java 11 --- discontinue Java 8 workaround; | changeset | files |
Fri, 06 Mar 2020 20:18:21 +0100 | wenzelm | support Java/VM monitoring via jconsole; | changeset | files |
Wed, 04 Mar 2020 21:09:02 +0100 | wenzelm | escape some special chars, notably for URL#NAME form; | changeset | files |