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;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 tip