diff options
author | Michael Schmidt <github@mschmidt.me> | 2016-05-10 19:13:18 +0200 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2016-05-10 19:13:18 +0200 |
commit | 812ae094557c60847de73c1e9ee198de9c17669d (patch) | |
tree | dfcda11db3d2406623be12d53786b87fa5504617 | |
parent | 470f207e9229b73dcaea889c531b016a34df3cc5 (diff) | |
download | compcert-812ae094557c60847de73c1e9ee198de9c17669d.tar.gz compcert-812ae094557c60847de73c1e9ee198de9c17669d.zip |
fix typo 'clinker_option' in configure for OSX
-rwxr-xr-x | configure | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -210,10 +210,10 @@ case "$target" in if [[ $kernel_major -gt 11 ]] then # OSX >= 10.8 - clinker_options="-arch i386 -Wl,-no_pie" ;; + clinker_options="-arch i386 -Wl,-no_pie" else # OSX <= 10.7 - clinker_options="-arch i386" ;; + clinker_options="-arch i386" fi libmath="";; ia32-cygwin) |