diff --git a/gtkui.py b/gtkui.py index 96981a433ceb2cc9fe78daaf8304c3e8510ed42f..cf4861f600dfdd28fec9971c191a00c8c754d248 100644 --- a/gtkui.py +++ b/gtkui.py @@ -335,6 +335,7 @@ much right right side if it *is* present. self.window.add(event_box) event_box.show() # catch clicks as end turn + event_box.set_extension_events(gtk.gdk.EXTENSION_EVENTS_ALL) event_box.set_events(gtk.gdk.BUTTON_PRESS_MASK) event_box.connect("button_press_event", self.end_turn) event_box.modify_bg(gtk.STATE_NORMAL, gtk.gdk.Color('black')) @@ -524,7 +525,7 @@ much right right side if it *is* present. self.window.fullscreen() self.fullscreen = not self.fullscreen - def end_turn(self, widget = None, data=None): + def end_turn(self, widget = None, event = None): """handle end turn events this passes the message to the gaming engine as quickly as @@ -548,6 +549,11 @@ much right right side if it *is* present. self.refresh() self.hilight() self.maybe_print("ended turn") + # mouse pointer debugging code, see #4511 + if event and event.device: + self.maybe_print("widget: %s" % widget) + self.maybe_print("device name: %s" % event.device.name) + self.maybe_print("device idt: %s" % event.deviceid) def handle_pause(self, widget, data=None, a=None, b=None): """pause handler