# HG changeset patch
# User wenzelm
# Date 1488816531 -3600
# Node ID 5d35f4bccfa799da40bc38fec6e292b0592ef0d1
# Parent  695930882487fc981154279a7ceeb151d01ca6bb
proper Text.Range.offside (NB: in Scala ~1 == -2);

diff -r 695930882487 -r 5d35f4bccfa7 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Mon Mar 06 17:05:57 2017 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Mon Mar 06 17:08:51 2017 +0100
@@ -69,7 +69,7 @@
             Pretty_Tooltip.invoke(() =>
               {
                 val rendering = JEdit_Rendering(snapshot, options)
-                val info = Text.Info(Text.Range(~1), body)
+                val info = Text.Info(Text.Range.offside, body)
                 Pretty_Tooltip(view, parent, new Point(x, y), rendering, Command.Results.empty, info)
               })
             null