From b372c0cf33681ef7e8ae3524987c5581fd3f92c0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 1 Jul 2019 00:16:40 +0200
Subject: [errors] Small cleanups and removal of dead code.

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

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 02682e2ee9..7c6fa8951b 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -392,7 +392,7 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc -> Some (Loc.unloc loc)
     | _        -> None in
-  let mk_msg () = CErrors.print ~info e in
+  let mk_msg () = CErrors.iprint (e,info) in
   match e with
   | e ->
       match Stateid.get info with
-- 
cgit v1.2.3