diff options
| author | Gaëtan Gilbert | 2018-02-02 16:03:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-02 16:03:37 +0100 |
| commit | a16be5c566a989e3ba02117ebd912d6025fd54fb (patch) | |
| tree | 719add667553f3fddb9e86860ee6bc104e34278a /dev/ci | |
| parent | e6353e9ef6542b444391a46d9557ebf3a6443947 (diff) | |
CClosure.unfold_projection: don't catch Not_found, assume env is ok
We can do this after the parent commit (Reductionops.nf_* don't use
empty env)
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions