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. --- library/goptions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index 0459417fb..b98cdac6a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -36,7 +36,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type") + user_err "Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) -- cgit v1.2.3