summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2019-07-30 10:44:00 +0100
committerDavid Allsopp <david.allsopp@metastack.com>2019-07-30 10:44:00 +0100
commit5bdf58f7d4515c889544bcd8c0a23119fa6d0987 (patch)
treeb0bbb554aba6eff28db757c7bc4fbb7d4af870e1
parent1e610e2703927144786c2e62907cd07e28677a0f (diff)
downloadocaml-5bdf58f7d4515c889544bcd8c0a23119fa6d0987.tar.gz
Regenerate configure
-rwxr-xr-xconfigure4
1 files changed, 3 insertions, 1 deletions
diff --git a/configure b/configure
index 0de9771d33..2d78aa9635 100755
--- a/configure
+++ b/configure
@@ -13520,6 +13520,8 @@ fi; system=elf ;; #(
arch=arm; model=armv5te; system=linux_eabi ;; #(
armv5*-*-linux-gnueabi) :
arch=arm; model=armv5; system=linux_eabi ;; #(
+ arm*-*-linux-gnueabihf) :
+ arch=arm; system=linux_eabihf ;; #(
arm*-*-linux-gnueabi) :
arch=arm; system=linux_eabi ;; #(
arm*-*-openbsd*) :
@@ -13744,7 +13746,7 @@ case $host in #(
esac
if test -n "$host_alias"; then :
- toolpref="${host}-"
+ toolpref="${host_alias}-"
else
toolpref=""
fi