Mon, 25 Mar 2024 19:57:01 +0100 merged
wenzelm [Mon, 25 Mar 2024 19:57:01 +0100] rev 79989
merged
Mon, 25 Mar 2024 19:56:12 +0100 misc updates, tuning and clarification;
wenzelm [Mon, 25 Mar 2024 19:56:12 +0100] rev 79988
misc updates, tuning and clarification;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 tip