diff options
| author | Vincent Laporte | 2019-06-06 16:03:41 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-06-06 16:03:41 +0000 |
| commit | f841689a74a0456ecec63659ef5e7f568fb60ba0 (patch) | |
| tree | 59e9defb7e77fbb385499820c487a23fcfe56f48 /kernel/write_uint63.ml | |
| parent | c5798a8e041abf0b021c0820f7e6a5436729827e (diff) | |
| parent | 1df461d41634d1d1dc330f0aca99921d3fced1fd (diff) | |
Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: vbgl
Diffstat (limited to 'kernel/write_uint63.ml')
| -rw-r--r-- | kernel/write_uint63.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index beb59ce205..42bb5dfbb1 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -31,8 +31,8 @@ let ml_file_copy input output = let write_uint63 () = ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_x86.ml" - else (* 64 bits *) "uint63_amd64.ml") + (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" + else (* 64 bits *) "uint63_amd64_63.ml") "uint63.ml" let () = write_uint63 () |