diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 8dda4773e..db0f96715 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 |