diff options
| author | Emilio Jesus Gallego Arias | 2019-02-08 18:54:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-08 18:54:13 +0100 |
| commit | d8cf6da35a1b1c697e8bd3017de607c4a2d89691 (patch) | |
| tree | 91246b016eddb78b63a91c9c6836257d6d0887eb /stm | |
| parent | 92df98da23057a47a6cd2053618fd97efe54ba30 (diff) | |
| parent | 6e052101b827a0abef83bc6a54da83e30f70bc94 (diff) | |
Merge PR #9525: Remove global output_native_objects flag.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 5 | ||||
| -rw-r--r-- | stm/stm.mli | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e7833f253e..b4f26570c6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2890,11 +2890,12 @@ let handle_failure (e, info) vcs = VCS.print (); Exninfo.iraise (e, info) -let snapshot_vio ~doc ldir long_f_dot_vo = +let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo = let doc = finish ~doc in if List.length (VCS.branches ()) > 1 then CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); - Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo + Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects + ldir long_f_dot_vo (Global.opaque_tables ()); doc diff --git a/stm/stm.mli b/stm/stm.mli index 313ac58111..102e832d3e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -160,7 +160,7 @@ val join : doc:doc -> doc - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one of the completed tasks is a failure) *) -val snapshot_vio : doc:doc -> DirPath.t -> string -> doc +val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) |