summaryrefslogtreecommitdiff
path: root/.ci/ci-make-benchmark.sh
diff options
context:
space:
mode:
Diffstat (limited to '.ci/ci-make-benchmark.sh')
-rwxr-xr-x.ci/ci-make-benchmark.sh3
1 files changed, 3 insertions, 0 deletions
diff --git a/.ci/ci-make-benchmark.sh b/.ci/ci-make-benchmark.sh
index d1689a2844..1fe0f9796f 100755
--- a/.ci/ci-make-benchmark.sh
+++ b/.ci/ci-make-benchmark.sh
@@ -5,6 +5,9 @@ set -e
5if [ "$1" = "release-ready" ] ; then 5if [ "$1" = "release-ready" ] ; then
6 exit 0 6 exit 0
7fi 7fi
8if [ "$1" = "coverity" ] ; then
9 exit 0
10fi
8travis_fold benchmark "ninja benchmark" 11travis_fold benchmark "ninja benchmark"
9echo "Nothing to do here, the benchmarks don't seem to terminate" 12echo "Nothing to do here, the benchmarks don't seem to terminate"
10#else 13#else