diff --git a/build/tools/before_install.sh b/build/tools/before_install.sh index 0ad23f4d18..e207adcc7c 100755 --- a/build/tools/before_install.sh +++ b/build/tools/before_install.sh @@ -11,6 +11,13 @@ SUDO=sudo case $(uname -s) in Linux) if [ -f /etc/apt/sources.list ]; then + # Show information about the repositories and priorities used. + echo 'APT sources used:' + $SUDO grep --no-messages '^[^#]' /etc/apt/sources.list /etc/apt/sources.list.d/* || true + echo 'APT preferences:' + $SUDO grep --no-messages '^[^#]' /etc/apt/preferences /etc/apt/preferences.d/* || true + echo '--- End of APT files dump ---' + run_apt() { echo "Running apt-get $@"