From 5b2d1c010aa0deb8b5ac89a9c9cdaa263e3b9d64 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 1 Oct 2020 20:42:43 +0200
Subject: Turn coq_float64.h into a .c file as it is no longer needed by
 coq_interp.c.

---
 kernel/byterun/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/byterun/dune')

diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 2998178be2..d3e2a2fa7f 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -4,7 +4,7 @@
  (public_name coq.vm)
  (foreign_stubs
   (language c)
-  (names coq_fix_code coq_memory coq_values coq_interp)
+  (names coq_fix_code coq_float64 coq_memory coq_values coq_interp)
   (flags (:include %{project_root}/config/dune.c_flags))))
 
 (rule
-- 
cgit v1.2.3