Fri, 04 Apr 2025 10:58:39 +0200 tuned signature;
wenzelm [Fri, 04 Apr 2025 10:58:39 +0200] rev 82424
tuned signature;
Fri, 04 Apr 2025 10:54:37 +0200 unused;
wenzelm [Fri, 04 Apr 2025 10:54:37 +0200] rev 82423
unused;
Thu, 03 Apr 2025 12:52:04 +0200 suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
wenzelm [Thu, 03 Apr 2025 12:52:04 +0200] rev 82422
suppress NavigatorPlugin and its dependencies -- requires to update jedit component;
Thu, 03 Apr 2025 12:37:14 +0200 prefer search bar (with navigation buttons) over old-fashioned tool bar -- requires to update jedit component;
wenzelm [Thu, 03 Apr 2025 12:37:14 +0200] rev 82421
prefer search bar (with navigation buttons) over old-fashioned tool bar -- requires to update jedit component;
Thu, 03 Apr 2025 12:04:13 +0200 add navigation buttons to search bar, depending on property "navigate-toolbar" -- requires to update jedit component;
wenzelm [Thu, 03 Apr 2025 12:04:13 +0200] rev 82420
add navigation buttons to search bar, depending on property "navigate-toolbar" -- requires to update jedit component;
Wed, 02 Apr 2025 23:22:59 +0200 remove goto_buffer in favour of uniform goto_file;
wenzelm [Wed, 02 Apr 2025 23:22:59 +0200] rev 82419
remove goto_buffer in favour of uniform goto_file;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 tip