tuned --- accomodate scala3;
authorwenzelm
Sat, 09 Apr 2022 11:45:39 +0200
changeset 75423 d164bf04d05e
parent 75422 6c3190da9701
child 75424 5f8f0bf8c72c
tuned --- accomodate scala3;
src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Sat Apr 09 11:41:37 2022 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Sat Apr 09 11:45:39 2022 +0200
@@ -107,7 +107,7 @@
 
           def indent_indent(tok: Token): Int =
             if (keywords.is_command(tok, keyword_open)) indent_size
-            else if (keywords.is_command(tok, keyword_close)) - indent_size
+            else if (keywords.is_command(tok, keyword_close)) { - indent_size }
             else 0
 
           def indent_offset(tok: Token): Int =