aboutsummaryrefslogtreecommitdiff
path: root/kernel/dune
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/dune')
-rw-r--r--kernel/dune7
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/dune b/kernel/dune
index ce6fdc03df..bd663974da 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -3,7 +3,7 @@
(synopsis "The Coq Kernel")
(public_name coq.kernel)
(wrapped false)
- (modules (:standard \ genOpcodeFiles uint63_31 uint63_63))
+ (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
(libraries lib byterun dynlink))
(executable
@@ -19,6 +19,11 @@
(deps (:gen-file uint63_%{ocaml-config:int_size}.ml))
(action (copy# %{gen-file} %{targets})))
+(rule
+ (targets float64.ml)
+ (deps (:gen-file float64_%{ocaml-config:int_size}.ml))
+ (action (copy# %{gen-file} %{targets})))
+
(documentation
(package coq))