Tue, 19 Nov 2024 10:11:17 +0100 unused;
wenzelm [Tue, 19 Nov 2024 10:11:17 +0100] rev 81485
unused;
Mon, 18 Nov 2024 16:48:11 +0100 tuned output: formatting is pointless for proportional font;
wenzelm [Mon, 18 Nov 2024 16:48:11 +0100] rev 81484
tuned output: formatting is pointless for proportional font;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 tip