Thu, 26 Dec 2024 15:18:19 +0100 | wenzelm | drop redundant space in HTML (see also 18a720984855); | changeset | files |
Thu, 26 Dec 2024 13:44:10 +0100 | wenzelm | clarified signature; | changeset | files |
Thu, 26 Dec 2024 13:22:28 +0100 | wenzelm | more robust: proper HTML.output; | changeset | files |
Thu, 26 Dec 2024 12:46:45 +0100 | wenzelm | tuned signature; | changeset | files |
Thu, 26 Dec 2024 12:38:25 +0100 | wenzelm | tuned: fewer warnings in IntelliJ IDEA; | changeset | files |
Thu, 26 Dec 2024 12:08:05 +0100 | wenzelm | clarified output; | changeset | files |
Thu, 26 Dec 2024 12:03:56 +0100 | wenzelm | clarified signature; | changeset | files |
Tue, 24 Dec 2024 16:57:28 +0100 | wenzelm | more GUI styles; | changeset | files |