aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/Clightgen.ml7
1 files changed, 6 insertions, 1 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index f272c3ed..eddb36e2 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -168,7 +168,12 @@ let _ =
| "arm" -> if Configuration.is_big_endian
then Machine.arm_bigendian
else Machine.arm_littleendian
- | "ia32" -> Machine.x86_32
+ | "x86" -> if Configuration.model = "64" then
+ Machine.x86_64
+ else
+ if Configuration.abi = "macosx"
+ then Machine.x86_32_macosx
+ else Machine.x86_32
| _ -> assert false
end;
Builtins.set C2C.builtins;