diff options
| author | Pierre Courtieu | 2021-01-22 14:45:08 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2021-02-03 17:15:01 +0100 |
| commit | 570744638ab4b08286562c0f4d45a7928ed008b0 (patch) | |
| tree | 75bba9ef80c938a90afb653410aace2974054b2c /lib/objFile.ml | |
| parent | 8615aac5fc342b2184b3431abec15dbab621efba (diff) | |
Fix #13739 - disable some warnings when calling Function.
Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions