Fri, 04 Apr 2025 22:11:29 +0200 update jedit component;
wenzelm [Fri, 04 Apr 2025 22:11:29 +0200] rev 82438
update jedit component;
Fri, 04 Apr 2025 21:48:51 +0200 more navigator positions;
wenzelm [Fri, 04 Apr 2025 21:48:51 +0200] rev 82437
more navigator positions;
Fri, 04 Apr 2025 20:34:13 +0200 clarified navigator events: avoid excessive 0 positions;
wenzelm [Fri, 04 Apr 2025 20:34:13 +0200] rev 82436
clarified navigator events: avoid excessive 0 positions;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 tip