diff options
| author | Hugo Herbelin | 2020-09-15 18:57:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-15 19:09:04 +0200 |
| commit | ec30b8515ee44bfe2ccf4297dab6f0e31e84572b (patch) | |
| tree | c1075201a1908a2d3a5ebe0477bd408d69e1a046 /lib/objFile.mli | |
| parent | c7f1e26f3ef4862e7fc72ce76167a4c7549a2205 (diff) | |
A temporary fix of #13018 and #12775 for branch 8.2.
We arbitrarily use max_int as higher level of custom entries in
printing, which should be ok since only < and <= are used to decide
when to use coercions.
Diffstat (limited to 'lib/objFile.mli')
0 files changed, 0 insertions, 0 deletions