From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 01:58:04 +0200
Subject: Remove errorlabstrm in favor of user_err

As noted by @ppedrot, the first is redundant. The patch is basically a renaming.

We didn't make the component optional yet, but this could happen in a
future patch.
---
 ide/ide_slave.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 8dda4773ef..db0f967151 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -300,7 +300,7 @@ let dirpath_of_string_list s =
   let id =
     try Nametab.full_name_module qid
     with Not_found ->
-      CErrors.errorlabstrm "Search.interface_search"
+      CErrors.user_err "Search.interface_search"
         (str "Module " ++ str path ++ str " not found.")
   in
   id
-- 
cgit v1.2.3