diff options
| author | Enrico Tassi | 2014-12-27 20:40:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-27 20:40:28 +0100 |
| commit | 1801eab1c6685f3d1a0311ac1074f252efcccbc5 (patch) | |
| tree | af3cc6d4619e5bc88af813d34248bf8183c1e746 | |
| parent | 68cec014db63283ce0f7941e6df5f5fc0dd6435f (diff) | |
STM: fix processing of errors
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 42500651cb..6558252a7a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -661,8 +661,8 @@ end = struct (* {{{ *) | Some _ -> (e, info) | None -> let loc = Option.default Loc.ghost (Loc.get_loc info) in - Hooks.(call execution_error id loc (iprint (e, info))); let (e, info) = Hooks.(call_process_error_once (e, info)) in + Hooks.(call execution_error id loc (iprint (e, info))); (e, Stateid.add info ?valid id) let same_env { system = s1 } { system = s2 } = |