tuned whitespace;
authorwenzelm
Sun Feb 23 18:18:40 2014 +0100 (2014-02-23)
changeset 55691aeba7cd45400
parent 55690 d73949233c2e
child 55692 19e8b00684f7
tuned whitespace;
src/Tools/jEdit/src/jedit_lib.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 16:08:38 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 18:18:40 2014 +0100
     1.3 @@ -172,7 +172,8 @@
     1.4            Text.Range(offset, offset + 2)
     1.5          else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
     1.6            Text.Range(offset - 1, offset + 1)
     1.7 -        else Text.Range(offset, offset + 1)
     1.8 +        else
     1.9 +          Text.Range(offset, offset + 1)
    1.10        }
    1.11        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
    1.12      }