diff options
| author | Hugo Herbelin | 2017-06-27 11:31:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-06-28 12:31:11 +0200 |
| commit | d01e3b07470ab326f5754332ac812f21794721bc (patch) | |
| tree | 0a6c2db31cd1987f6ef18633974c6c20148b00dd /API/API.mli | |
| parent | ebfed8fc20c6cad1eddd5057d191905b42630b4e (diff) | |
A fix for #5598 (no discharge of Existing Classes referring to local variables).
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions