diff options
| author | Enrico Tassi | 2018-10-03 16:29:09 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-10-03 16:34:23 +0200 |
| commit | d5d57b5e5cb7c39f2ed7312fe1464873ba795c7e (patch) | |
| tree | 4b21e567a67b23432826e5bbffc47b1b04b07ddf /kernel/cClosure.mli | |
| parent | 10477a2b31e9cddc697b03f75adcc5e42acb0e85 (diff) | |
[build] enable warnings ok kernel/% in make based builds
This is to sync with the dune build system that sets these warnings
Diffstat (limited to 'kernel/cClosure.mli')
0 files changed, 0 insertions, 0 deletions