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.ml | |
| parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) | |
Add XML protocol support for Wait.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 3386044f2..7e17fa2f5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2373,6 +2373,7 @@ let finish () = | _ -> () let wait () = + finish (); Slaves.wait_all_done (); VCS.print () @@ -2386,7 +2387,6 @@ let rec join_admitted_proofs id = | _ -> join_admitted_proofs view.next let join () = - finish (); wait (); stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); @@ -2486,7 +2486,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) match c with (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm (VtWait, b), VtNow -> wait (); `Ok | VtStm ((VtJoinDocument|VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater.") |