diff options
| author | Enrico Tassi | 2019-01-10 11:20:25 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-10 11:20:25 +0100 |
| commit | 2eae13f396833e582697be6a0b3513fc169b8053 (patch) | |
| tree | 629cbfbf868a9467574ca9af0c7ab10f76e3ea44 | |
| parent | f28ffe175f8a3f80c6b7e48734b3592a31899ba9 (diff) | |
| parent | f7d362d04d788ede814d0e090b916aa512eb8a6c (diff) | |
Merge PR #9331: [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 4a1e64eb4a..036b8d7969 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 | _ -> |