aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b89d93c1..4bd08a88 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -536,9 +536,12 @@ let _ =
| "arm" -> if Configuration.is_big_endian
then Machine.arm_bigendian
else Machine.arm_littleendian
- | "ia32" -> if Configuration.abi = "macosx"
- then Machine.x86_32_macosx
- else Machine.x86_32
+ | "ia32" -> 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;