diff options
| author | Maxime Dénès | 2019-01-09 17:13:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-09 17:13:41 +0100 |
| commit | f7d362d04d788ede814d0e090b916aa512eb8a6c (patch) | |
| tree | 70250cb0aa565f1a3efa5ff87255f0e6f4225d73 | |
| parent | 727d4da625f88b7ba302d5c129f9773dc1fb1e33 (diff) | |
[STM] Fix semantics of `cur_id` w.r.t. error states
| -rw-r--r-- | stm/stm.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 32c6c7d959..7e4ee38547 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -869,7 +869,6 @@ end = struct (* {{{ *) cur_id := id | { state = Error ie } -> - cur_id := id; Exninfo.iraise ie | _ -> |