Fri, 04 Apr 2025 22:20:23 +0200 wenzelm NEWS;
Fri, 04 Apr 2025 22:12:21 +0200 wenzelm more documentation;
Fri, 04 Apr 2025 22:11:29 +0200 wenzelm update jedit component;
Fri, 04 Apr 2025 21:48:51 +0200 wenzelm more navigator positions;
Fri, 04 Apr 2025 20:34:13 +0200 wenzelm clarified navigator events: avoid excessive 0 positions;
Fri, 04 Apr 2025 20:31:57 +0200 wenzelm more robust: make double-sure that get_text does not crash (see on non-existent file);
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 tip