--- a/src/Tools/jEdit/patches/main Sat Aug 23 18:49:06 2025 +0200
+++ b/src/Tools/jEdit/patches/main Sat Aug 23 18:54:22 2025 +0200
@@ -377,9 +377,9 @@
clear.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
jEdit.getProperty("remove-all-markers.label")));
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
+diff -Nru 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-05-20 13:46:50.541586193 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-08-23 18:50:05.907962159 +0200
@@ -8,13 +8,15 @@
###
@@ -563,7 +563,15 @@
Blank24.gif
#}}}
-@@ -163,31 +166,31 @@
+@@ -144,6 +147,7 @@
+ new-file-in-mode \
+ open-file \
+ %recent-files \
++ %recent-directories \
+ - \
+ reload \
+ reload-all \
+@@ -163,31 +167,31 @@
print \
- \
exit
@@ -614,7 +622,7 @@
#}}}
#{{{ Edit menu
-@@ -211,12 +214,12 @@
+@@ -211,12 +215,12 @@
%text \
%indent \
%source
@@ -633,7 +641,7 @@
#{{{ More Clipboard menu
clipboard=cut-append \
-@@ -308,16 +311,18 @@
+@@ -308,16 +312,18 @@
regexp \
- \
hypersearch-results
@@ -662,7 +670,7 @@
#}}}
#{{{ Markers menu
-@@ -336,12 +341,12 @@
+@@ -336,12 +342,12 @@
view-markers \
-
markers.code=new MarkersProvider();
@@ -681,7 +689,7 @@
#}}}
#{{{ Folding menu
-@@ -388,9 +393,12 @@
+@@ -388,9 +394,12 @@
- \
set-view-title \
toggle-full-screen
@@ -697,6 +705,14 @@
#{{{ Scrolling menu
scrolling=scroll-to-current-line \
+@@ -436,7 +445,6 @@
+
+ #{{{ Utilities menu
+ utils=vfs.browser \
+- %recent-directories \
+ - \
+ %favorites \
+ %current-directory \
@@ -454,9 +462,9 @@
- \
%quick-options