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.

diff --git a/.travis.yml b/.travis.yml
index 1f09a78fa6bc3f5cefaae50ba96a7166e5768b92..fc135868715fd3f954d39227bcf7df95d8659e17 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -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"

diff --git a/scripts/coverity.sh b/tools/coverity.sh
similarity index 100%
rename from scripts/coverity.sh
rename to tools/coverity.sh