diff options
| author | Enrico Tassi | 2014-09-09 13:10:48 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-09 13:11:38 +0200 |
| commit | 6129d83ad15799b6b9318a1c4fa5fc73ddbb5ad9 (patch) | |
| tree | 39cf17d6c5ec2c57cb19f7d46e9fdd0352217631 | |
| parent | e62aa755e79fbdf69e1073c272ae417fbe9e2a4f (diff) | |
A marshalling failure does not make a worker `Old
| -rw-r--r-- | stm/asyncTaskQueue.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |