diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-18 11:35:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-19 11:43:41 +0200 |
| commit | d87bc5b9fb353655f8b905d73293abe96b0ad063 (patch) | |
| tree | a552df12fe9ab4bfd8575999b1945dea03e2c274 /stm/stm.mli | |
| parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) | |
Add XML protocol support for Wait.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 188b176ba..3f01fca01 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -51,6 +51,9 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] (* Evaluates the tip of the current branch *) val finish : unit -> unit +(* Internal use (fake_ide) only, do not use *) +val wait : unit -> unit + val observe : Stateid.t -> unit val stop_worker : string -> unit |