diff options
| author | Gaëtan Gilbert | 2019-02-08 14:10:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 14:10:22 +0100 |
| commit | 95e723892c336808aad0926c675f3e0ac8ba7d99 (patch) | |
| tree | 939aec8d4659c02ab5c5f29c4f74b59f1d50ecd7 /toplevel/ccompile.ml | |
| parent | bb967f18247fc79c7158a89a1fe160a558910460 (diff) | |
Remove global output_native_objects flag.
Diffstat (limited to 'toplevel/ccompile.ml')
| -rw-r--r-- | toplevel/ccompile.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index df2b983029..31656e0b07 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -125,7 +125,8 @@ let compile opts copts ~echo ~f_in ~f_out = let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); + let output_native_objects = opts.output_native_objects in + Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ()); Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); @@ -168,7 +169,8 @@ let compile opts copts ~echo ~f_in ~f_out = let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); - let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in + let output_native_objects = opts.output_native_objects in + let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in Stm.reset_task_queue () | Vio2Vo -> |