src/Tools/jEdit/patches/search_bar
author wenzelm
Tue, 22 Apr 2025 22:11:16 +0200
changeset 82565 1033ed5d3972
parent 82420 0fc508521b2a
permissions -rw-r--r--
tuned signature -- requires to update jedit component;

diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java	2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java	2025-04-03 11:33:23.921426197 +0200
@@ -51,6 +51,10 @@
 		setFloatable(false);
 		add(Box.createHorizontalStrut(2));
 
+		if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) {
+			add(GUIUtilities.loadToolBar("navigate-toolbar"));
+		}
+
 		JLabel label = new JLabel(jEdit.getProperty("view.search.find"));
 		add(label);