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 /dev/base_include | |
| 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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions