diff options
| author | Hugo Herbelin | 2015-07-16 21:34:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-16 21:43:53 +0200 |
| commit | 0b3a335219e161dc04f6734e9ee4f7c08cde6cd5 (patch) | |
| tree | 325ab45b64832fa7e55d85cf7446517d40fd04df /kernel/nativelib.ml | |
| parent | 916a8dc2c6b1dd8400d5c44b5d9c7fc793cc0e97 (diff) | |
Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions