diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-09 15:55:07 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-09 15:55:07 +0100 |
| commit | 32205e08619fa8fce63caaf46a289d1868982a0a (patch) | |
| tree | c13fa64981785902f68009ec7a8170496cf5a7a9 /Makefile | |
| parent | 251bd245dd2709ffd553a2dec48e05853acc0cf7 (diff) | |
| download | compcert-32205e08619fa8fce63caaf46a289d1868982a0a.tar.gz compcert-32205e08619fa8fce63caaf46a289d1868982a0a.zip | |
More tweaking of module 'open'
I really like to have Floats and Values opened. The other opens I can live without, but Floats.Float.zero is just wrong.
Diffstat (limited to 'Makefile')
0 files changed, 0 insertions, 0 deletions