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 /Makefile.checker | |
| parent | 77e3b3c43aebe9ad18ac99b34cf6dfac1ecc93fd (diff) | |
[warnings] Disable warning 58 "no cmx file was found in path"
Diffstat (limited to 'Makefile.checker')
0 files changed, 0 insertions, 0 deletions