diff options
Diffstat (limited to 'toplevel/stm.mli')
| -rw-r--r-- | toplevel/stm.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/stm.mli b/toplevel/stm.mli index 4949845b5..89efdc718 100644 --- a/toplevel/stm.mli +++ b/toplevel/stm.mli @@ -44,6 +44,9 @@ val join : unit -> unit type tasks val dump : unit -> tasks +val check_task : tasks -> int -> unit +val info_tasks : tasks -> (string * float * int) list + (* Id of the tip of the current branch *) val get_current_state : unit -> Stateid.t |