aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/pp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 4f50e3e19b..3fcb6ac595 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -508,7 +508,7 @@ let get_id_for_feedback () = !feedback_id, !feedback_route
(** Utility *)
let string_of_ppcmds c =
- msg_with Format.str_formatter c;
+ Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
Format.flush_str_formatter ()
let log_via_feedback () = logger := (fun ~id lvl msg ->