aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2013-12-24 17:56:11 +0100
committerEnrico Tassi2013-12-24 18:23:41 +0100
commitc59a8d40e80f3d00081e26739a5aa5eba01269e0 (patch)
tree1e35b481a580881d6f165163098321ed6be37f56
parent96d137ce97bf469235ac04dfb824bc89af7255bc (diff)
cleanup warning
-rw-r--r--toplevel/stm.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 5f1c31e42a..d05fce8b69 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -865,12 +865,14 @@ end = struct (* {{{ *)
assign (`Val pl);
(* We restart the slave, to avoid memory leaks. We could just
Pp.feedback (Interface.InProgress ~-1) *)
+ last_task := None;
raise KillRespawn
| TaskBuildProof(_,_,_, assign,_,_), RespError (err_id,valid,e) ->
let e = Stateid.add ~valid (RemoteException e) err_id in
assign (`Exn e);
(* We restart the slave, to avoid memory leaks. We could just
Pp.feedback (Interface.InProgress ~-1) *)
+ last_task := None;
raise KillRespawn
| _, RespGetCounterFreshLocalUniv ->
marshal_more_data oc (MoreDataLocalUniv
@@ -888,7 +890,7 @@ end = struct (* {{{ *)
if !cancel_switch then raise KillRespawn else loop ()
| _, RespFeedback _ -> assert false (* Parsing in master process *)
in
- loop (); last_task := None
+ loop ()
with
| VCS.Expired -> (* task cancelled: e.g. the user did backtrack *)
Pp.feedback (Interface.InProgress ~-1);