diff --git a/ci/install-build-deps.sh b/ci/install-build-deps.sh index 4dc913a8..dda00623 100755 --- a/ci/install-build-deps.sh +++ b/ci/install-build-deps.sh @@ -25,6 +25,9 @@ if [ -z "$GITHUB_ACTIONS" ]; then GITHUB_PATH=/dev/null fi +# Use non-default mirror for Ubuntu packages, because the default mirror currently have problems. +$SUDO_CMD sed -i -E -e 's!http://(archive|security).ubuntu.com!http://europe-west2.gce.archive.ubuntu.com!g' /etc/apt/sources.list + case "$ID-$VERSION_ID" in ubuntu-20.04|ubuntu-22.04) # Curl must be available to get the repo key below.