diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-05 02:01:56 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-07 22:56:56 +0100 |
| commit | 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 (patch) | |
| tree | 9af84a7fbc95a55c976c9d0529828cc87fb831b3 /plugins/extraction | |
| parent | 69c4e7cfa0271f024b2178082e4be2e3ca3be263 (diff) | |
Extraction: remove the "print to devnull" hack now that pp isn't lazy anymore
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |