From d77ec8a5c6d76d5bd78490474dcc238ab8fc7b40 Mon Sep 17 00:00:00 2001
From: Dundar Goc <gocdundar@gmail.com>
Date: Mon, 11 Jul 2022 16:40:49 +0200
Subject: ci: remove unnecessary file ci/script.sh

It only runs run_tests.sh and checks coverage, which can be replaced by
just moving the coverage check to ci/run_tests.sh.
---
 ci/script.sh | 12 ------------
 1 file changed, 12 deletions(-)
 delete mode 100755 ci/script.sh

(limited to 'ci/script.sh')

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