From 980431c745997587a9463ead5bdf849e872ce1ad Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 12 Dec 2018 12:53:19 +0100
Subject: [stm] join the tip of the document even when fixing a proof (fix
 #9204)

---
 stm/stm.ml | 4 ++--
 1 file 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
 
-- 
cgit v1.2.3