Quelle  props   Sprache: Text

diff -ru jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props
--- jedit5.7.0/jEdit/org/jedit/localization/jedit_en.props 2024-08-03 19:53:22.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/jedit/localization/jedit_en.props 2025-04-22 22:08:19.298392180 +0200
@@ -70,7 +70,7 @@
 #}}}
 
 #{{{ Tool bar
-view.search.find=Search for:
+view.search.find=Search:
 view.search.close-tooltip=Hide search bar (ESCAPE)
 
 view.action.prompt=Action:
@@ -1282,8 +1282,7 @@
  The most likely reason is that the JAR file is corrupt; try\n\
  reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
  for a full stack trace.
-plugin-error.start-error=Cannot start: {0}\n\
- Try updating to a newer version of the plugin.
+plugin-error.start-error=Cannot start: {0}
 plugin-error.already-loaded=Two copies installed. Please remove one of the \
  two copies.
 plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
@@ -1610,7 +1609,7 @@
 options.gutter.optionalComponents=Optional gutter components
 options.gutter.lineNumbers=Line numbers
 options.gutter.minLineNumberDigits=Minimal number of digits to reserve for line numbers:
-options.gutter.selectionAreaEnabled=Line selection area when line numbers are not shown
+options.gutter.selectionAreaEnabled=Line selection area (with icons) when line numbers are not shown
 options.gutter.selectionAreaBgColor=Selection area background color:
 options.gutter.selectionAreaWidth=Selection area width (in pixels):
 options.gutter.font=Gutter font: