| Mon, 10 May 2021 22:18:12 +0200 | wenzelm | put more resources into jedit_build component; | changeset | files |
| Mon, 10 May 2021 20:09:47 +0200 | wenzelm | more brackets (see f6b453449cc6); | changeset | files |
| Mon, 10 May 2021 18:31:18 +0200 | wenzelm | more brackets; | changeset | files |