From 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 5 Feb 2017 02:01:56 +0100 Subject: Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore --- plugins/extraction/extract_env.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/extraction/extract_env.ml') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 52f22ee60..e019bb3c2 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -507,8 +507,7 @@ let print_structure_to_file (fn,si,mo) dry struc = in (* First, a dry run, for computing objects to rename or duplicate *) set_phase Pre; - let devnull = formatter true None in - pp_with devnull (d.pp_struct struc); + ignore (d.pp_struct struc); let opened = opened_libraries () in (* Print the implementation *) let cout = if dry then None else Option.map open_out fn in -- cgit v1.2.3