diff options
| author | Enrico Tassi | 2014-01-06 16:14:16 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-06 16:54:51 +0100 |
| commit | 183a35d7b6eaaa377ecda21d32b3bf183ecea9dd (patch) | |
| tree | 6c5603c02cb2ec6147a4889e1363a308e6f3200e | |
| parent | c44a12ab9136b8d13cec0d9c1f3837b6f92eb283 (diff) | |
STM: handle side effects of workers correctly
| -rw-r--r-- | toplevel/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 790a651079..ee6305b5b1 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -790,7 +790,7 @@ end = struct (* {{{ *) | Declarations.SEsubproof(_, { Declarations.const_body = Declarations.OpaqueDef f; const_constraints = cst} ) -> - ignore(Future.force f); ignore(Future.force cst) + ignore(Future.join f); ignore(Future.join cst) | _ -> ()) se) l; l) in |