aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/dune
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/dune')
-rw-r--r--kernel/byterun/dune2
1 files changed, 1 insertions, 1 deletions
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