--- a/src/Tools/jEdit/patches/icons Thu Apr 17 00:07:15 2025 +0200
+++ b/src/Tools/jEdit/patches/icons Thu Apr 17 00:25:58 2025 +0200
@@ -148,8 +148,8 @@
clear.addActionListener(this);
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props 2024-08-03 19:53:20.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-04-17 00:01:14.063978204 +0200
-@@ -8,11 +8,11 @@
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-04-17 00:11:31.583536114 +0200
+@@ -8,13 +8,15 @@
###
#{{{ Common icons
@@ -165,8 +165,12 @@
+common.clearAll.icon=32x32/actions/edit-clear.svg?scale=0.7
logo.icon.small=16x16/apps/jedit.png
logo.icon.medium=32x32/apps/jedit.png
++navigate-backwards.icon=idea-icons/expui/general/chevronLeft.svg?scale=1.2
++navigate-forwards.icon=idea-icons/expui/general/chevronRight.svg?scale=1.2
-@@ -28,7 +28,7 @@
+ #}}}
+
+@@ -28,7 +30,7 @@
defer=false
startup=true
@@ -175,7 +179,7 @@
dropdown-arrow.icon=ToolbarMenu.gif
#}}}
-@@ -39,68 +39,69 @@
+@@ -39,68 +41,69 @@
buffer-options combined-options - \
plugin-manager - help
@@ -296,7 +300,7 @@
22x22/actions/application-run.png \
22x22/actions/edit-find-multiple.png \
22x22/actions/edit-find-single.png \
-@@ -109,18 +110,18 @@
+@@ -109,18 +112,18 @@
22x22/actions/window-unsplit.png \
22x22/actions/zoom-in.png \
22x22/actions/zoom-out.png \
@@ -326,7 +330,7 @@
Blank24.gif
#}}}
-@@ -163,31 +164,31 @@
+@@ -163,31 +166,31 @@
print \
- \
exit
@@ -377,7 +381,7 @@
#}}}
#{{{ Edit menu
-@@ -211,12 +212,12 @@
+@@ -211,12 +214,12 @@
%text \
%indent \
%source
@@ -396,7 +400,7 @@
#{{{ More Clipboard menu
clipboard=cut-append \
-@@ -308,16 +309,18 @@
+@@ -308,16 +311,18 @@
regexp \
- \
hypersearch-results
@@ -425,7 +429,7 @@
#}}}
#{{{ Markers menu
-@@ -336,12 +339,12 @@
+@@ -336,12 +341,12 @@
view-markers \
-
markers.code=new MarkersProvider();
@@ -444,7 +448,7 @@
#}}}
#{{{ Folding menu
-@@ -388,9 +391,12 @@
+@@ -388,9 +393,12 @@
- \
set-view-title \
toggle-full-screen
@@ -460,7 +464,7 @@
#{{{ Scrolling menu
scrolling=scroll-to-current-line \
-@@ -454,9 +460,9 @@
+@@ -454,9 +462,9 @@
- \
%quick-options
@@ -473,7 +477,7 @@
#{{{ Recent Directories menu
recent-directories.code=new RecentDirectoriesProvider();
-@@ -518,9 +524,9 @@
+@@ -518,9 +526,9 @@
rescan-macros \
-
macros.code=new MacrosProvider();
@@ -486,7 +490,7 @@
#}}}
#{{{ Plugins menu
-@@ -771,7 +777,7 @@
+@@ -771,7 +779,7 @@
#{{{ HyperSearch results dialog
hypersearch-results.clear.icon=22x22/actions/edit-clear.png
@@ -495,7 +499,7 @@
hypersearch-results.multi.multiple.icon=22x22/actions/edit-find-multiple.png
hypersearch-results.multi.single.icon=22x22/actions/edit-find-single.png
hypersearch-results.match.highlight.icon=22x22/actions/edit-find-highlight-match.png
-@@ -784,8 +790,8 @@
+@@ -784,8 +792,8 @@
#}}}
#{{{ Help Viewer
@@ -506,7 +510,7 @@
#}}}
#}}}
-@@ -809,9 +815,9 @@
+@@ -809,9 +817,9 @@
#{{{ Abbreviations pane
options.abbrevs.code=new AbbrevsOptionPane();
@@ -519,7 +523,7 @@
#}}}
#{{{ Appearance pane
-@@ -840,11 +846,11 @@
+@@ -840,11 +848,11 @@
#{{{ Context Menu pane
options.context.code=new ContextOptionPane();
@@ -536,7 +540,7 @@
options.context.includeOptionsLink=true
#}}}
-@@ -906,12 +912,12 @@
+@@ -906,12 +914,12 @@
#{{{ Tool Bar pane
options.toolbar.code=new ToolBarOptionPane();
@@ -555,7 +559,7 @@
#}}}
#{{{ View pane
-@@ -949,7 +955,8 @@
+@@ -949,7 +957,8 @@
vfs.browser.default-filter=*[^~#]
vfs.browser.filter-enabled=true
vfs.browser.file.icon=16x16/mimetypes/text-x-generic.png
@@ -565,7 +569,7 @@
vfs.browser.open-file.icon=16x16/actions/edit-select-all.png
vfs.browser.dir.icon=16x16/places/folder.png
vfs.browser.open-dir.icon=16x16/status/folder-open.png
-@@ -1007,13 +1014,13 @@
+@@ -1007,13 +1016,13 @@
plugin-manager.mirror-url=http://plugins.jedit.org/export/mirror_list.php
#{{{ Plugin management