From d87aca813d13930b2d8f67fbc7ea03dabdb48410 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 13 Sep 2013 15:44:17 +0000
Subject: fix STM feeback on running jobs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16776 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9310591416..b71b5c4be0 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -723,6 +723,7 @@ end = struct (* {{{ *)
             loop (); last_task := None
         with
         | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *)
+            Pp.feedback (Interface.InProgress ~-1);
             prerr_endline ("Task expired: " ^ pr_task task)
         | MarshalError ->
             msg_warning(strbrk("Marshalling error. "^
@@ -787,10 +788,12 @@ end = struct (* {{{ *)
       | e when Errors.noncritical e ->
         (* This can happen if the proof is broken.  The error has also been
          * signalled as a feedback, hence we can silently recover *)
+        Pp.feedback (Interface.InProgress ~-1);
         marshal_response !slave_oc (RespError (print e));
         prerr_endline "Slave: failed with the following exception:";
         prerr_endline (string_of_ppcmds (print e))
       | e ->
+        Pp.feedback (Interface.InProgress ~-1);
         msg_error(str"Slave: failed with the following CRITICAL exception:");
         msg_error(print e);
         msg_error(str"Slave: bailing out");
-- 
cgit v1.2.3