# HG changeset patch
# User wenzelm
# Date 1742907187 -3600
# Node ID a01c1f8743622d9b61c29afbe0fffd09866f1b10
# Parent  4238ebc9918d94c9500acb9504969a0c7afb8e11
tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;

diff -r 4238ebc9918d -r a01c1f874362 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Mar 25 09:10:44 2025 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Mar 25 13:53:07 2025 +0100
@@ -266,7 +266,7 @@
 
   /* search */
 
-  private val search_label: Component = new Label("Search:") {
+  private val search_label: Component = new Label(jEdit.getProperty("search.find")) {
     tooltip = "Search and highlight output via regular expression"
   }