From cbd7317516eaac4a5f37c896da5ea984ec1bb77a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 10 Apr 2014 16:09:22 +0200
Subject: CoqIDE: removing a timer may raise an exception

---
 ide/ideutils.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'ide/ideutils.ml')

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 2ae46fc7e..d8ca34f98 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -130,7 +130,10 @@ let mktimer () =
     kill =
       (fun () -> match !timer with
         | None -> ()
-        | Some id -> GMain.Timeout.remove id; timer := None) }
+        | Some id ->
+            (try GMain.Timeout.remove id
+             with Glib.GError _ -> ());
+             timer := None) }
 
 let last_dir = ref ""
 
-- 
cgit v1.2.3