coverage.sh: don't attempt deleting non-existant directory

main
parent 067daaf4c2
commit 5fd1ca62d9
Signed by untrusted user: josch
GPG Key ID: F2CBA5C78FBD83E1

@ -603,7 +603,7 @@ if [ "\$ret" = 0 ]; then
echo expected failure but got exit \$ret >&2
exit 1
fi
rm -r /tmp/debian-chroot
[ ! -e /tmp/debian-chroot ]
END
if [ "$CONTAINER" = "lxc" ]; then
# see https://stackoverflow.com/questions/65748254/

Loading…
Cancel
Save