From f8fdc27f922694edf74a7b608de1596e0a1ac0e3 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 19 Apr 2019 15:29:53 +0200
Subject: Make primitive float work on Windows

---
 kernel/byterun/coq_interp.c | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel')

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;
-- 
cgit v1.2.3