diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-24 18:09:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-10-24 18:09:12 +0200 |
| commit | a49d3b267754eae6036e0c03e48bff7e1c028a58 (patch) | |
| tree | 57adee99aff6e9afbe1dbb18ca4e1e7809466abf /Makefile | |
| parent | c4746b43f5d035d26d1d0c3bb0164f00544889e4 (diff) | |
| download | compcert-kvx-a49d3b267754eae6036e0c03e48bff7e1c028a58.tar.gz compcert-kvx-a49d3b267754eae6036e0c03e48bff7e1c028a58.zip | |
Tune behavior wrt warnings:
- cchecklink was compiled with -warn-error, which is bad for production code
- silence warning 3 (deprecated functions)
- silence warning 20 (unused function argument) for Coq-extracted files.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1 |
1 files changed, 0 insertions, 1 deletions
@@ -41,7 +41,6 @@ OCB_OPTIONS=\ OCB_OPTIONS_CHECKLINK=\ $(OCB_OPTIONS) \ -I checklink \ - -cflags "-w -3" \ -use-ocamlfind OCB_OPTIONS_CLIGHTGEN=\ $(OCB_OPTIONS) \ |