diff options
| author | Gaëtan Gilbert | 2018-08-23 09:35:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-28 12:48:46 +0200 |
| commit | e705297921639fa0aef7d6e50e58d50257de3160 (patch) | |
| tree | b2576dd961761620736c820fbb4c39875dc7004d /kernel | |
| parent | f885e8a88620351d9dc4b0969f520d13197f2184 (diff) | |
Fix #7795: UGraph.AlreadyDeclared with Program
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions