From 2f61ea2926a72ba3d7b5cb8a1746e34df99838cc Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 1 Dec 2014 10:06:54 +0100
Subject: Remove dead code

---
 ide/ideutils.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'ide/ideutils.ml')

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 006b41cc40..a38c672e2e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -61,9 +61,6 @@ let byte_offset_to_char_offset s byte_offset =
 
 let glib_utf8_pos_to_offset s ~off = byte_offset_to_char_offset s off
 
-let print_id id =
-  Minilib.log ("GOT sig id :"^(string_of_int (Obj.magic id)))
-
 let do_convert s =
   let from_loc () =
     let _,char_set = Glib.Convert.get_charset () in
-- 
cgit v1.2.3