diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9f10b2502a..b1f4177579 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -472,7 +472,7 @@ let print_xml = with e -> let e = Errors.push e in Mutex.unlock m; iraise e -let slave_logger xml_oc level message = +let slave_logger xml_oc ?loc level message = (* convert the message into XML *) let msg = hov 0 message in let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in |