author | wenzelm |
Tue, 25 Mar 2025 13:53:07 +0100 | |
changeset 82402 | a01c1f874362 |
parent 82342 | 4238ebc9918d |
child 82403 | 6e80327eb30a |
--- 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" }