Fri, 27 Dec 2024 17:35:24 +0100 tuned GUI output: more uniform;
wenzelm [Fri, 27 Dec 2024 17:35:24 +0100] rev 81671
tuned GUI output: more uniform;
Fri, 27 Dec 2024 17:30:59 +0100 minor performance tuning;
wenzelm [Fri, 27 Dec 2024 17:30:59 +0100] rev 81670
minor performance tuning;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 tip