Sat, 13 Aug 2022 11:18:46 +0200 | wenzelm | tuned whitespace; | changeset | files |
Sat, 13 Aug 2022 11:18:22 +0200 | wenzelm | tuned, following hints by IntelliJ IDEA; | changeset | files |
Fri, 12 Aug 2022 20:21:09 +0200 | wenzelm | merged | changeset | files |
Fri, 12 Aug 2022 20:20:53 +0200 | wenzelm | more GUI elements; | changeset | files |