From dd47fcfc08c43288a49797cc72829da3f9642094 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 11 Nov 2016 10:57:47 +0100
Subject: Making explicit that a result is discarded (ocaml warning).

---
 ide/preferences.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/preferences.ml')

diff --git a/ide/preferences.ml b/ide/preferences.ml
index 64327d74f..b16d45b54 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -468,7 +468,7 @@ let create_tag name default =
   let iter table =
     let tag = GText.tag ~name () in
     table#add tag#as_tag;
-    pref#connect#changed (fun _ -> set_tag tag);
+    ignore (pref#connect#changed (fun _ -> set_tag tag));
     set_tag tag;
   in
   List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
-- 
cgit v1.2.3