From ace202e17e7f41aa3347618426b334be3d9f0e17 Mon Sep 17 00:00:00 2001
From: Ebrahim Byagowi <ebrahim@gnu.org>
Date: Tue, 28 Apr 2020 19:38:04 +0430
Subject: [PATCH] [ci] remove trigger-coverity.sh

hopefully not needed, we are submitting it in a bot
---
 .ci/trigger-coverity.sh | 11 -----------
 1 file changed, 11 deletions(-)
 delete mode 100644 .ci/trigger-coverity.sh

diff --git a/.ci/trigger-coverity.sh b/.ci/trigger-coverity.sh
deleted file mode 100644
index 19852bd11..000000000
--- a/.ci/trigger-coverity.sh
+++ /dev/null
@@ -1,11 +0,0 @@
-#!/bin/bash
-
-set -x
-set -o errexit -o nounset
-
-if test x"$TRAVIS_EVENT_TYPE" != x"cron"; then exit; fi
-if test x"$TRAVIS_BRANCH" != x"master"; then exit; fi
-
-git fetch --unshallow
-git remote add upstream "https://$GH_TOKEN@github.com/harfbuzz/harfbuzz.git"
-git push -q upstream master:coverity_scan