aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/xmlprotocol.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/xmlprotocol.ml')
-rw-r--r--ide/xmlprotocol.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 79509fe02..aecb317bc 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -607,7 +607,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
| PrintAst x -> mkGood (handler.print_ast x)
| Annotate x -> mkGood (handler.annotate x)
with any ->
- let any = Errors.push any in
+ let any = CErrors.push any in
Fail (handler.handle_exn any)
(** brain dead code, edit if protocol messages are added/removed *)