aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.mli
diff options
context:
space:
mode:
Diffstat (limited to 'lib/feedback.mli')
-rw-r--r--lib/feedback.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 62b909516..37f38c8ff 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -94,8 +94,9 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit
consequences. *)
val msg_error : ?loc:Loc.t -> Pp.t -> unit
-(** Message indicating that something went really wrong, though still
- recoverable; otherwise an exception would have been raised. *)
+[@@ocaml.deprecated "msg_error is an internal function and should not be \
+ used unless you know what you are doing. Use \
+ [CErrors.user_err] instead."]
val msg_debug : ?loc:Loc.t -> Pp.t -> unit
(** For debugging purposes *)