Rename scripts/coverity.sh to tools/coverity.sh

There are only two files in tools/, I don't think we need a separate
directory for them.
This commit is contained in:
Zbigniew Jędrzejewski-Szmek 2018-03-12 15:39:21 +01:00
parent d14829c8b7
commit 748c59b110
2 changed files with 1 additions and 1 deletions

View File

@ -96,7 +96,7 @@ jobs:
-v ${TOOL_BASE}:${TOOL_BASE}:ro \
--name travis_coverity_scan ${DOCKER_REPOSITORY}:${TRAVIS_COMMIT} bash
# Make sure Coverity script is executable
- docker cp scripts/coverity.sh travis_coverity_scan:/usr/local/bin
- docker cp tools/coverity.sh travis_coverity_scan:/usr/local/bin
# Preconfigure with meson to prevent Coverity from capturing meson metadata
# Set compiler flag to prevent emit failure
- docker exec -it travis_coverity_scan sh -c "CFLAGS='-D_Float128=long\ double' meson cov-build -Dman=false"