diff options
| -rwxr-xr-x | .ci/ci-make-check.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/.ci/ci-make-check.sh b/.ci/ci-make-check.sh index a069ad92de..38e00c1ac6 100755 --- a/.ci/ci-make-check.sh +++ b/.ci/ci-make-check.sh @@ -4,6 +4,12 @@ if [ "$1" = "release-ready" ] ; then exit 0 fi + +#T7151 +if [ "$1" = "misc" ] || [ "$1" = "misc-disabled" ] ; then + exit 0 +fi + travis_fold check "make check-TESTS" if [ "$DISTRO" != "" ] ; then for tries in 1 2 3 ; do |