Thu, 26 Dec 2024 15:18:19 +0100 wenzelm drop redundant space in HTML (see also 18a720984855);
Thu, 26 Dec 2024 13:44:10 +0100 wenzelm clarified signature;
Thu, 26 Dec 2024 13:22:28 +0100 wenzelm more robust: proper HTML.output;
Thu, 26 Dec 2024 12:46:45 +0100 wenzelm tuned signature;
Thu, 26 Dec 2024 12:38:25 +0100 wenzelm tuned: fewer warnings in IntelliJ IDEA;
Thu, 26 Dec 2024 12:08:05 +0100 wenzelm clarified output;
Thu, 26 Dec 2024 12:03:56 +0100 wenzelm clarified signature;
Tue, 24 Dec 2024 16:57:28 +0100 wenzelm more GUI styles;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -8 +8 +10 +30 +100 tip