Tue, 22 Apr 2025 22:10:59 +0200 tuned GUI -- requires to update jedit component;
wenzelm [Tue, 22 Apr 2025 22:10:59 +0200] rev 82564
tuned GUI -- requires to update jedit component;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -1 +1 +10 +30 tip