diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/ide_slave.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 6e0a3c787b..8b8de43ee1 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -400,9 +400,10 @@ let eval_call c = let slave_logger level message = (* convert the message into XML *) + let msg = Pp.string_of_ppcmds (hov 0 message) in let message = { Interface.message_level = level; - Interface.message_content = Pp.string_of_ppcmds message + Interface.message_content = msg; } in let xml = Serialize.of_message message in (* Send it to stdout *) |