diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/configure b/configure index ce0c6a01f1..7337823652 100755 --- a/configure +++ b/configure @@ -3742,6 +3742,18 @@ if test "$build_pt_chown" = yes; then fi +# The abi-tags file uses a fairly simplistic model for name recognition that +# can't distinguish i486-pc-linux-gnu fully from i486-pc-gnu. So we mutate a +# $host_os of `gnu*' here to be `gnu-gnu*' just so that it can tell. +# This doesn't get used much beyond that, so it's fairly safe. +case "$host_os" in +linux*) + ;; +gnu*) + host_os=`echo $host_os | sed -e 's/gnu/gnu-gnu/'` + ;; +esac + # We keep the original values in `$config_*' and never modify them, so we # can write them unchanged into config.make. Everything else uses # $machine, $vendor, and $os, and changes them whenever convenient. |