Thu, 03 Mar 2022 16:18:27 +0100 misc tuning, based on suggestions by IntelliJ IDEA;
wenzelm [Thu, 03 Mar 2022 16:18:27 +0100] rev 75200
misc tuning, based on suggestions by IntelliJ IDEA;
Thu, 03 Mar 2022 16:05:02 +0100 clarified signature;
wenzelm [Thu, 03 Mar 2022 16:05:02 +0100] rev 75199
clarified signature;
Thu, 03 Mar 2022 15:47:54 +0100 tuned signature;
wenzelm [Thu, 03 Mar 2022 15:47:54 +0100] rev 75198
tuned signature;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 tip