# HG changeset patch
# User wenzelm
# Date 1649497539 -7200
# Node ID d164bf04d05e0dfca34247886a9d6987c35fec46
# Parent  6c3190da97012d864940804a614d75e93526681e
tuned --- accomodate scala3;

diff -r 6c3190da9701 -r d164bf04d05e 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 =