equal
deleted
inserted
replaced
|
1 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 |
|
2 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200 |
|
3 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-04-03 11:33:23.921426197 +0200 |
|
4 @@ -51,6 +51,10 @@ |
|
5 setFloatable(false); |
|
6 add(Box.createHorizontalStrut(2)); |
|
7 |
|
8 + if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) { |
|
9 + add(GUIUtilities.loadToolBar("navigate-toolbar")); |
|
10 + } |
|
11 + |
|
12 JLabel label = new JLabel(jEdit.getProperty("view.search.find")); |
|
13 add(label); |
|
14 |