From 7ddd9da1306b7f394c25db8080d9de14ae8b9c58 Mon Sep 17 00:00:00 2001 From: Vadim Zeitlin Date: Tue, 2 Nov 2021 19:48:53 +0100 Subject: Update the apt sources before trying to install anything We need to refresh the information about the available packages before trying to install them. --- Tools/CI-linux-install.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Tools/CI-linux-install.sh b/Tools/CI-linux-install.sh index 04dd5127f..b18206e64 100644 --- a/Tools/CI-linux-install.sh +++ b/Tools/CI-linux-install.sh @@ -7,6 +7,8 @@ if [[ -n "$GCC" ]]; then $RETRY sudo add-apt-repository -y ppa:ubuntu-toolchain-r/test $RETRY sudo apt-get -qq update $RETRY sudo apt-get install -qq g++-$GCC +else + $RETRY sudo apt-get -qq update fi $RETRY sudo apt-get -qq install libboost-dev libpcre3-dev -- cgit v1.2.1