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 /lib/Floats.v | |
| parent | c4746b43f5d035d26d1d0c3bb0164f00544889e4 (diff) | |
| download | compcert-a49d3b267754eae6036e0c03e48bff7e1c028a58.tar.gz compcert-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 'lib/Floats.v')
0 files changed, 0 insertions, 0 deletions