1 files changed, 0 insertions, 12 deletions
diff --git a/ci/script.sh b/ci/script.sh
deleted file mode 100755
index 74fc4eda6c..0000000000
--- a/ci/script.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-set -o pipefail
-
-ci/run_${CI_TARGET}.sh
-
-if [[ -s "${GCOV_ERROR_FILE}" ]]; then
-  echo '=== Unexpected gcov errors: ==='
-  cat "${GCOV_ERROR_FILE}"
-  exit 1
-fi