diff options
| author | Enrico Tassi | 2013-12-24 17:56:11 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2013-12-24 18:23:41 +0100 |
| commit | c59a8d40e80f3d00081e26739a5aa5eba01269e0 (patch) | |
| tree | 1e35b481a580881d6f165163098321ed6be37f56 | |
| parent | 96d137ce97bf469235ac04dfb824bc89af7255bc (diff) | |
cleanup warning
| -rw-r--r-- | toplevel/stm.ml | 4 |
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); |
