# HG changeset patch
# User wenzelm
# Date 1649102660 -7200
# Node ID 42fe20507496014316751c033c57946362b620e9
# Parent  010a77180dff799ea4b87b0f60b74e07eb265e97
proper indentation (relevant for scala3);

diff -r 010a77180dff -r 42fe20507496 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Apr 03 09:07:37 2022 +0000
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Mon Apr 04 22:04:20 2022 +0200
@@ -139,7 +139,7 @@
         revalidate()
         repaint()
       }
-      search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
+    search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
   }