Sat, 23 Dec 2023 19:08:35 +0100 eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
wenzelm [Sat, 23 Dec 2023 19:08:35 +0100] rev 79340
eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
Sat, 23 Dec 2023 16:12:53 +0100 minor performance tuning: shorter names;
wenzelm [Sat, 23 Dec 2023 16:12:53 +0100] rev 79339
minor performance tuning: shorter names;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 tip