Fri, 17 Jan 2025 11:01:44 +0100 misc tuning and clarification;
wenzelm [Fri, 17 Jan 2025 11:01:44 +0100] rev 81840
misc tuning and clarification;
Fri, 17 Jan 2025 10:56:10 +0100 tuned;
wenzelm [Fri, 17 Jan 2025 10:56:10 +0100] rev 81839
tuned;
Fri, 17 Jan 2025 10:53:30 +0100 clarified make_type: proper make_name;
wenzelm [Fri, 17 Jan 2025 10:53:30 +0100] rev 81838
clarified make_type: proper make_name;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip