Browse code

Change the cursor when you're over a jump point.

From: Marius Gedminas <marius@gedmin.as>

Jose.R.Fonseca authored on 13/07/2008 03:21:51
Showing 1 changed files

  • xdot.py index bfdac38..9e133e4 100755
... ...
@@ -732,6 +732,8 @@ class NullAction(DragAction):
732 732
         dot_widget = self.dot_widget
733 733
         if dot_widget.get_url(event.x, event.y) is not None:
734 734
             dot_widget.window.set_cursor(gtk.gdk.Cursor(gtk.gdk.HAND2))
735
+        elif dot_widget.get_jump(event.x, event.y) is not None:
736
+            dot_widget.window.set_cursor(gtk.gdk.Cursor(gtk.gdk.HAND1))
735 737
         else:
736 738
             dot_widget.window.set_cursor(gtk.gdk.Cursor(gtk.gdk.ARROW))
737 739