# HG changeset patch
# User wenzelm
# Date 1393175920 -3600
# Node ID aeba7cd454000a896feda724910c130a4e623317
# Parent  d73949233c2e05df9419ac8684fc109ba0cb7f8d
tuned whitespace;

diff -r d73949233c2e -r aeba7cd45400 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 16:08:38 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Feb 23 18:18:40 2014 +0100
@@ -172,7 +172,8 @@
           Text.Range(offset, offset + 2)
         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
           Text.Range(offset - 1, offset + 1)
-        else Text.Range(offset, offset + 1)
+        else
+          Text.Range(offset, offset + 1)
       }
       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
     }