aboutsummaryrefslogtreecommitdiff
path: root/ide/xmlprotocol.ml
diff options
context:
space:
mode:
authorPierre Corbineau2014-12-16 15:59:52 +0100
committerPierre Corbineau2014-12-16 16:01:25 +0100
commit8029f7555f9c6f201cc70b5ecc538b11a861f0aa (patch)
treec750b3ea7cafd5ec2176866bbd16208e5335978a /ide/xmlprotocol.ml
parentd4f5bdd6f7304fac541bb5f4555ecdd6aa42699a (diff)
parentf88cce2698da000ab9054da31330db70997a41a4 (diff)
fix bug #2447 in congruence
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 da0bcaf0b9..0cd7e7b818 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 *)