diff options
Diffstat (limited to 'stdlib/format.ml')
| -rw-r--r-- | stdlib/format.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/stdlib/format.ml b/stdlib/format.ml index d3b3843d95..e36e2c0b12 100644 --- a/stdlib/format.ml +++ b/stdlib/format.ml @@ -566,12 +566,11 @@ let pp_set_formatter_output_functions state f g = let pp_get_formatter_output_functions state () = (state.pp_output_function, state.pp_flush_function);; -let pp_set_all_formatter_output_functions state f g h i = +let pp_set_all_formatter_output_functions state + ~out:f ~flush:g ~newline:h ~spaces:i = pp_set_formatter_output_functions state f g; state.pp_output_newline <- (function _ -> function () -> h ()); state.pp_output_spaces <- (function _ -> function n -> i n);; -let pp_set_all_formatter_output_functions' state ~out ~flush ~newline ~space = - pp_set_all_formatter_output_functions state out flush newline space let pp_get_all_formatter_output_functions state () = (state.pp_output_function, state.pp_flush_function, state.pp_output_newline state, state.pp_output_spaces state);; @@ -692,8 +691,6 @@ and get_formatter_output_functions = and set_all_formatter_output_functions = pp_set_all_formatter_output_functions std_formatter -and set_all_formatter_output_functions' = - pp_set_all_formatter_output_functions' std_formatter and get_all_formatter_output_functions = pp_get_all_formatter_output_functions std_formatter;; |