summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-20 13:15:48 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-08-20 13:15:48 +0000
commit7a2725740d4cf204cb38d281e5c2e14e0f6ccf0f (patch)
tree508ff2164f68ac9719de792fe2d2fb2ee2af5162
parent7c8039725e25f642898503b772e6043c7cbbf983 (diff)
Better validation of target for ARM
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rwxr-xr-xconfigure6
1 files changed, 5 insertions, 1 deletions
diff --git a/configure b/configure
index a47b59d..787bd90 100755
--- a/configure
+++ b/configure
@@ -115,8 +115,12 @@ case "$target" in
exit 2;;
esac
case "$target" in
- *-eabi) abi="eabi";;
+ *-eabi|*-linux) abi="eabi";;
*-eabihf|*-hf|*-hardfloat) abi="hardfloat";;
+ *)
+ echo "Unknown target '$target'." 1>&2
+ echo "$usage" 1>&2
+ exit 2;;
esac
system="linux"
cc="${toolprefix}gcc"