diff options
| author | Enrico Tassi | 2018-12-12 12:53:19 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-13 10:09:32 +0100 |
| commit | 980431c745997587a9463ead5bdf849e872ce1ad (patch) | |
| tree | d458964bc04e01e55942c7056566f6d7f9197e92 | |
| parent | 84a950c8e1fa06d0dd764e9a426edbd987a7989e (diff) | |
[stm] join the tip of the document even when fixing a proof (fix #9204)
| -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 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 |