From 59e99e01a5f23f53bbfb4828e6a0639efa9235b5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 16 Jul 2014 15:02:48 +0200
Subject: STM: Goal printing got wrong in a merge, fixed

---
 stm/stm.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 4d29bbb38e..2895062edf 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -733,6 +733,7 @@ end = struct
 
   let slave_print_all_goals id =
     let rec aux id =
+      print_goals_of_state id;
       try aux (VCS.visit id).next
       with
       | VCS.Expired -> ()
@@ -1368,7 +1369,8 @@ let known_state ?(redefine_qed=false) ~cache id =
     if !Flags.async_proofs_mode = Flags.APonParallel 0 then
       Pp.feedback ~state_id:id Feedback.ProcessingInMaster;
     State.define ~cache:cache_step ~redefine:redefine_qed step id;
-    if !Flags.feedback_goals then print_goals_of_state id;
+    if !Flags.feedback_goals && not (Flags.async_proofs_is_worker ()) then
+      print_goals_of_state id;
     prerr_endline ("reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
-- 
cgit v1.2.3