diff options
| author | Emilio Jesus Gallego Arias | 2017-06-15 12:36:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-18 03:42:48 +0200 |
| commit | 11c52f0882b39afe853473f7a9289e62d1ca843a (patch) | |
| tree | e06789afa842f5fdd4ce51dced0a9cd1ddbb92d2 /API/grammar_API.ml | |
| 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 'API/grammar_API.ml')
0 files changed, 0 insertions, 0 deletions