diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 20:14:45 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-12 16:24:04 +0200 |
commit | a069562bc0d4e82f6b1587864a8297b21a3250cc (patch) | |
tree | e53690330a5b3d417a40bc9f074c8fb5e64bb22e /checker/environ.ml | |
parent | 77e3b3c43aebe9ad18ac99b34cf6dfac1ecc93fd (diff) |
[warnings] Disable warning 58 "no cmx file was found in path"
Diffstat (limited to 'checker/environ.ml')
0 files changed, 0 insertions, 0 deletions