Mon, 14 Oct 2024 11:16:11 +0200 wenzelm tuned;
Mon, 14 Oct 2024 11:13:26 +0200 wenzelm tuned;
Mon, 14 Oct 2024 11:06:03 +0200 wenzelm tuned;
Sat, 12 Oct 2024 22:11:38 +0200 wenzelm merged
Sat, 12 Oct 2024 22:05:37 +0200 wenzelm misc tuning and clarification;
Sat, 12 Oct 2024 21:21:50 +0200 wenzelm tuned;
Sat, 12 Oct 2024 19:21:47 +0200 wenzelm tuned: more readable names;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 tip