author | wenzelm |
Sat, 09 Apr 2022 11:45:39 +0200 | |
changeset 75423 | d164bf04d05e |
parent 75422 | 6c3190da9701 |
child 75424 | 5f8f0bf8c72c |
--- 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 =