diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 13:48:15 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-16 14:23:56 +0200 |
| commit | 7ded7df853fd0485822f2a9c79207352af5dca38 (patch) | |
| tree | 09fd579374bab505782d809d16767dd7d43653df /ide/serialize.ml | |
| parent | f9a619753644ba8e0f0ca1218396c8efee52b544 (diff) | |
ideslave: do not bail out in case of XML error
Used to be an `exit 1`, now an error message is printed on stderr.
This helps people experimenting with the XML protocol.
Diffstat (limited to 'ide/serialize.ml')
0 files changed, 0 insertions, 0 deletions