diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-30 18:15:58 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-30 18:15:58 +0100 |
commit | b49c80406f518d273056b2143f55e23deeea2813 (patch) | |
tree | 3376811ee5d80bb779477551b3d524bcc1b417bd /engine/termops.ml | |
parent | 668c2edc15aad38229eb46c022571df2cbf31079 (diff) |
Command.declare_definition: grab the fix_exn early (follows 77cf18e)
When a future is fully forced (joined), the fix_exn is dropped,
since joined futures are values (hence they cannot raise exceptions).
When a future for a transparent definition enters the environment
it is joined. If one needs to pick its fix_exn, he should do it
before that.
Diffstat (limited to 'engine/termops.ml')
0 files changed, 0 insertions, 0 deletions