coverage.sh: don't run make_mirror.sh
This commit is contained in:
parent
dde777123e
commit
6bbf3943d1
1 changed files with 4 additions and 1 deletions
|
@ -4,7 +4,10 @@ set -eu
|
||||||
|
|
||||||
mirrordir="./shared/cache/debian"
|
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
|
# we use -f because the file might not exist
|
||||||
rm -f shared/cover_db.img
|
rm -f shared/cover_db.img
|
||||||
|
|
Loading…
Reference in a new issue