tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;
authorwenzelm
Tue, 25 Mar 2025 13:53:07 +0100
changeset 82402 a01c1f874362
parent 82342 4238ebc9918d
child 82403 6e80327eb30a
tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;
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"
   }