diff options
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 75aa08e7b..d77c19cfb 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -48,7 +48,8 @@ val stop_worker : string -> unit val join : unit -> unit (* To save to disk an incomplete document *) type tasks -val dump : (Future.UUID.t * int) list -> tasks +val dump_final : int Future.UUIDMap.t -> tasks +val dump_snapshot : int Future.UUIDMap.t -> tasks val check_task : string -> tasks -> int -> bool val info_tasks : tasks -> (string * float * int) list |