diff options
| author | Brian Campbell | 2019-02-08 18:06:23 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-02-08 18:17:23 +0000 |
| commit | 60897fea38949960d3f0e1370bbf73f157e099ec (patch) | |
| tree | f9abde0a8323eed478e38b19107ae318ce09714e /src/profile.ml | |
| parent | 44e35e2384824f8f3b3cc65a61bbb76e08a6422c (diff) | |
Prevent top_sort throwing away overloads (and other multiple definitions)
Previously it would quietly throw away all definitions for an id except one.
This usually doesn't matter, but some rewrites use overloaded identifiers
and can break if the definition is lost.
Diffstat (limited to 'src/profile.ml')
0 files changed, 0 insertions, 0 deletions