diff options
| -rwxr-xr-x | autogen.sh | 7 | ||||
| -rw-r--r-- | distro-configs/Jenkins/linux_gcc_release_64 | 1 |
2 files changed, 8 insertions, 0 deletions
diff --git a/autogen.sh b/autogen.sh index 8c0bb0ade4ba..478aed6944b5 100755 --- a/autogen.sh +++ b/autogen.sh @@ -151,6 +151,13 @@ if (defined $ENV{LODE_HOME}) $ENV{PATH}="$ENV{LODE_HOME}/opt/bin:$ENV{PATH}"; print STDERR "add LODE_HOME/opt/bin in PATH\n"; } + # For the Config=linux_gcc_release_64 Jenkins jobs that build on CentOS against Developer + # Toolset 7: + if (-d '/opt/rh/devtoolset-7/root/usr/bin') + { + $ENV{PATH}="/opt/rh/devtoolset-7/root/usr/bin:$ENV{PATH}"; + print STDERR "added /opt/rh/devtoolset-7/root/usr/bin to PATH\n"; + } } my $aclocal_flags = $ENV{ACLOCAL_FLAGS}; diff --git a/distro-configs/Jenkins/linux_gcc_release_64 b/distro-configs/Jenkins/linux_gcc_release_64 index 8b137891791f..962c332840de 100644 --- a/distro-configs/Jenkins/linux_gcc_release_64 +++ b/distro-configs/Jenkins/linux_gcc_release_64 @@ -1 +1,2 @@ +--disable-werror |