[gedit] externaltools: use Gdk.CURRENT_TIME

[Ignacio Casal Quinteiro <icq src gnome org>]

commit b6086cab8c664d2cfb3e5b4a6d33c215d1b207da
Author: Ignacio Casal Quinteiro <icq gnome org>
Date:   Sun Dec 25 19:45:33 2011 +0100

    externaltools: use Gdk.CURRENT_TIME

 plugins/externaltools/tools/manager.py |    4 ++--
 1 files changed, 2 insertions(+), 2 deletions(-)
---
diff --git a/plugins/externaltools/tools/manager.py b/plugins/externaltools/tools/manager.py
index d353a3e..f1f7cc7 100644
--- a/plugins/externaltools/tools/manager.py
+++ b/plugins/externaltools/tools/manager.py
@@ -184,8 +184,8 @@ class LanguagesPopup(Gtk.Window):
 
     def do_destroy(self):
         if self.keyboard:
-            self.keyboard.ungrab(0L)
-        self.pointer.ungrab(0L)
+            self.keyboard.ungrab(Gdk.CURRENT_TIME)
+        self.pointer.ungrab(Gdk.CURRENT_TIME)
 
         return Gtk.Window.do_destroy(self)