diff options
| author | Emilio Jesus Gallego Arias | 2019-04-20 15:18:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-21 20:25:20 +0200 |
| commit | 1df461d41634d1d1dc330f0aca99921d3fced1fd (patch) | |
| tree | ab3283af9033ea1e8ab24b34bef1ade3ee77f948 /kernel/dune | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
[build] Select uint63 using `ocamlc -config` variables.
This seems more robust and avoids having another implementation of
`cp`.
Diffstat (limited to 'kernel/dune')
| -rw-r--r-- | kernel/dune | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/kernel/dune b/kernel/dune index 5b23a705ae..4038bf5638 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_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) (libraries lib byterun dynlink)) (executable @@ -14,15 +14,10 @@ (targets copcodes.ml) (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) -(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}))) + (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (action (copy# %{gen-file} %{targets}))) (documentation (package coq)) |