aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-10-01 20:42:43 +0200
committerGuillaume Melquiond2020-11-13 15:14:34 +0100
commit5b2d1c010aa0deb8b5ac89a9c9cdaa263e3b9d64 (patch)
tree0a2e8c3e8b2a13f610cccf8ec6ed5a56dbba4cf7 /Makefile.common
parent136454f306c8d4de83b8f37201307205a7c57786 (diff)
Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
1 files changed, 1 insertions, 1 deletions
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