diff options
Diffstat (limited to 'lib/pp.ml4')
| -rw-r--r-- | lib/pp.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 854e4b49c..c602b403e 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -332,3 +332,7 @@ let msgnl x = msgnl_with !std_ft x let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x + +let string_of_ppcmds c = + msg_with Format.str_formatter c; + Format.flush_str_formatter () |