diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index e019bb3c2..ee623c5ca 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -472,13 +472,14 @@ let formatter dry file = if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) else match file with - | Some f -> Pp_control.with_output_to f + | Some f -> Topfmt.with_output_to f | None -> Format.formatter_of_buffer buf in + (* XXX: Fixme, this shouldn't depend on Topfmt *) (* We never want to see ellipsis ... in extracted code *) Format.pp_set_max_boxes ft max_int; (* We reuse the width information given via "Set Printing Width" *) - (match Pp_control.get_margin () with + (match Topfmt.get_margin () with | None -> () | Some i -> Format.pp_set_margin ft i; |