Wed, 02 Oct 2024 13:34:03 +0200 clarified abbreviation;
wenzelm [Wed, 02 Oct 2024 13:34:03 +0200] rev 81101
clarified abbreviation;
Wed, 02 Oct 2024 11:27:19 +0200 tuned whitespace;
wenzelm [Wed, 02 Oct 2024 11:27:19 +0200] rev 81100
tuned whitespace;
Wed, 02 Oct 2024 11:17:47 +0200 tuned;
wenzelm [Wed, 02 Oct 2024 11:17:47 +0200] rev 81099
tuned;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 tip