diff --git a/infra/base-images/base-builder/compile b/infra/base-images/base-builder/compile index e60f86fd9..1a3d4f508 100755 --- a/infra/base-images/base-builder/compile +++ b/infra/base-images/base-builder/compile @@ -77,7 +77,7 @@ BUILD_CMD="bash -eux $SRC/build.sh" # We need to preserve source code files for generating a code coverage report. # We need exact files that were compiled, so copy both $SRC and $WORK dirs. -COPY_SOURCES_CMD="cp -rL --parents $SRC $WORK /usr/include $OUT" +COPY_SOURCES_CMD="cp -rL --parents $SRC $WORK /usr/include /usr/local/include $OUT" if [ "${BUILD_UID-0}" -ne "0" ]; then adduser -u $BUILD_UID --disabled-password --gecos '' builder