| Mon, 10 May 2021 19:45:51 +0000 | haftmann | guide is out of focus | changeset | files |
| Mon, 10 May 2021 22:32:02 +0200 | wenzelm | proper build for fresh target directory (amending d9823224fcfe); | changeset | files |
| Mon, 10 May 2021 22:18:12 +0200 | wenzelm | put more resources into jedit_build component; | changeset | files |