From 6bbf3943d15a84c07bdbb70ce759c2a996cd1327 Mon Sep 17 00:00:00 2001
From: Johannes 'josch' Schauer <josch@mister-muffin.de>
Date: Fri, 18 Oct 2019 22:46:23 +0200
Subject: [PATCH] coverage.sh: don't run make_mirror.sh

---
 coverage.sh | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/coverage.sh b/coverage.sh
index cf795f5..eb8ebd2 100755
--- a/coverage.sh
+++ b/coverage.sh
@@ -4,7 +4,10 @@ set -eu
 
 mirrordir="./shared/cache/debian"
 
-./make_mirror.sh
+if [ ! -e "$mirrordir" ]; then
+	echo "run ./make_mirror.sh before running $0" >&2
+	exit 1
+fi
 
 # we use -f because the file might not exist
 rm -f shared/cover_db.img