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