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.

---
 Makefile.common | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index caf1821ce5..1f59bff183 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -122,7 +122,7 @@ LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
 DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN)$(DLLEXT)
 
 BYTERUN:=$(addprefix kernel/byterun/, \
-  coq_fix_code.o coq_memory.o coq_values.o coq_interp.o )
+  coq_fix_code.o coq_float64.o coq_memory.o coq_values.o coq_interp.o )
 
 # LINK ORDER:
 # respecting this order is useful for developers that want to load or link
-- 
cgit v1.2.3