diff options
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/ci-install.sh | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tools/ci-install.sh b/tools/ci-install.sh index ca678ed..1b2fe7b 100755 --- a/tools/ci-install.sh +++ b/tools/ci-install.sh @@ -71,11 +71,6 @@ case "$ci_distro" in # Don't ask questions, just do it sudo="$sudo env DEBIAN_FRONTEND=noninteractive" - # Debian Docker images use httpredir.debian.org but it seems to be - # unreliable; use a CDN instead - $sudo sed -i -e 's/httpredir\.debian\.org/deb.debian.org/g' \ - /etc/apt/sources.list - $sudo apt-get -qq -y update $sudo apt-get -qq -y install --no-install-recommends \ |