diff options
| author | Pierre Roux | 2019-04-19 15:29:53 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:21:11 +0100 |
| commit | f8fdc27f922694edf74a7b608de1596e0a1ac0e3 (patch) | |
| tree | 8c101e668ea50a1c39420e432d0382edc40b98b2 /kernel/byterun | |
| parent | a2ba4016a64f84193261db9a52196adc39cb5767 (diff) | |
Make primitive float work on Windows
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index e67325eb9a..6e6adb1293 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1652,6 +1652,12 @@ value coq_interprete double f; print_instr("CHECKFRSHIFTEXP"); CheckFloat1(); + /* frexp(infinity) incorrectly returns nan on mingw */ +#if defined(__MINGW32__) || defined(__MINGW64__) + if (fpclassify(Double_val(accu)) == FP_INFINITE) { + f = Double_val(accu); + } else +#endif f = frexp(Double_val(accu), &exp); if (fpclassify(f) == FP_NORMAL) { exp += FLOAT_EXP_SHIFT; |