diff --git a/coverage.sh b/coverage.sh index ac127cb..d0ca786 100755 --- a/coverage.sh +++ b/coverage.sh @@ -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/