From 6129d83ad15799b6b9318a1c4fa5fc73ddbb5ad9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Sep 2014 13:10:48 +0200
Subject: A marshalling failure does not make a worker `Old

---
 stm/asyncTaskQueue.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm/asyncTaskQueue.ml')

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index cb03459cc5..74e83a39fd 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -186,7 +186,8 @@ module Make(T : Task) = struct
             match response with
             | Response resp ->
                 (match T.use_response task resp with
-                | `Stay -> last_task := None; giveback_token ()
+                | `Stay ->
+                     last_task := None; worker_age := `Old; giveback_token ()
                 | `StayReset -> last_task := None; raise KillRespawn)
             | RespGetCounterNewUnivLevel ->
                 marshal_more_data oc (MoreDataUnivLevel
@@ -209,7 +210,6 @@ module Make(T : Task) = struct
               string_of_ppcmds (print e));
             flush_all ()
         end;
-        worker_age := `Old;
       done;
       raise Die
     with
-- 
cgit v1.2.3