Tue, 25 Mar 2025 15:53:54 +0100 more robust;
wenzelm [Tue, 25 Mar 2025 15:53:54 +0100] rev 82404
more robust;
Tue, 25 Mar 2025 15:50:41 +0100 tuned: fewer warnings in IntelliJ IDEA;
wenzelm [Tue, 25 Mar 2025 15:50:41 +0100] rev 82403
tuned: fewer warnings in IntelliJ IDEA;
Tue, 25 Mar 2025 13:53:07 +0100 tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;
wenzelm [Tue, 25 Mar 2025 13:53:07 +0100] rev 82402
tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 tip