aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.ml')
-rw-r--r--stm/stm.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index e835bdcb1e..61b8140ae6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2715,7 +2715,7 @@ let finish ~doc =
); doc
let wait ~doc =
- let doc = finish ~doc in
+ let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in
Slaves.wait_all_done ();
VCS.print ();
doc
@@ -2734,7 +2734,7 @@ let join ~doc =
stm_prerr_endline (fun () -> "Joining the environment");
Global.join_safe_environment ();
stm_prerr_endline (fun () -> "Joining Admitted proofs");
- join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
+ join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master);
VCS.print ();
doc