diff options
Diffstat (limited to 'plugins/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 292ae7955d..588fe0cf23 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -470,10 +470,14 @@ let print_structure_to_file (fn,si,mo) dry struc = (* Print the implementation *) let cout = if dry then None else Option.map open_out fn in let ft = formatter dry cout in + let file_comment = + let split_comment = Str.split (Str.regexp "[ \t\n]+") (file_comment ()) in + prlist_with_sep spc str split_comment + in begin try (* The real printing of the implementation *) set_phase Impl; - pp_with ft (d.preamble mo opened unsafe_needs); + pp_with ft (d.preamble mo file_comment opened unsafe_needs); pp_with ft (d.pp_struct struc); Option.iter close_out cout; with e -> @@ -487,7 +491,7 @@ let print_structure_to_file (fn,si,mo) dry struc = let ft = formatter false (Some cout) in begin try set_phase Intf; - pp_with ft (d.sig_preamble mo opened unsafe_needs); + pp_with ft (d.sig_preamble mo file_comment opened unsafe_needs); pp_with ft (d.pp_sig (signature_of_structure struc)); close_out cout; with e -> |