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 /stm/stm.mli | |
| parent | bb967f18247fc79c7158a89a1fe160a558910460 (diff) | |
Remove global output_native_objects flag.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 821ab59a43..91651e3534 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -156,7 +156,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 *) |