diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-15 12:36:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-18 03:42:48 +0200 |
| commit | 11c52f0882b39afe853473f7a9289e62d1ca843a (patch) | |
| tree | e06789afa842f5fdd4ce51dced0a9cd1ddbb92d2 /ide | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
[ide] Better exn printing. [fixes BZ#5524]
Due to the situation explained in bug 5360, error printing in
ide_slave results in an anomaly. We fix that by properly processing
the error.
This fixes BZ#5524, however BZ#5525 , still applies.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9c771cbef..6298d9f09 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -341,6 +341,7 @@ let about () = { } let handle_exn (e, info) = + let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in let dummy = Stateid.dummy in let loc_of e = match Loc.get_loc e with | Some loc -> Some (Loc.unloc loc) |