diff options
| author | Julien Freche | 2020-07-14 10:56:47 -0700 |
|---|---|---|
| committer | Julien Freche | 2020-07-14 10:56:47 -0700 |
| commit | 3bf8126178f7d3aca41686b3759cf35e9284a06c (patch) | |
| tree | 269eadcced5018737ff407952e633d3cc3e1cc8d /src/initial_check.mli | |
| parent | 7d815832a9410a3975c6ec8438556916eab493eb (diff) | |
c2: primop: -O: make sure to pick global or name correctly
Diffstat (limited to 'src/initial_check.mli')
0 files changed, 0 insertions, 0 deletions