diff options
Diffstat (limited to 'kernel/dune')
| -rw-r--r-- | kernel/dune | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/kernel/dune b/kernel/dune index 01abdb8f67..1f2d696a36 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,13 +3,23 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules_without_implementation cinstr nativeinstr) + (modules (:standard \ uint63_x86 uint63_amd64 write_uint63)) (libraries lib byterun)) (rule (targets copcodes.ml) - (deps (:h-file byterun/coq_instruct.h) make-opcodes) - (action (run ./make_opcodes.sh %{h-file} %{targets}))) + (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh) + (action (bash "./make_opcodes.sh %{h-file} %{targets}"))) + +(executable + (name write_uint63) + (modules write_uint63) + (libraries unix)) + +(rule + (targets uint63.ml) + (deps (:gen ./write_uint63.exe) uint63_x86.ml uint63_amd64.ml) + (action (run %{gen}))) (documentation (package coq)) |