From d186dcdc32225960b459f716caccc39c82ae594a Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Sat, 6 Sep 2025 18:48:39 -0400 Subject: [PATCH] ci: avoid man page builds (#6398) --- ci/ci-install.bash | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ci/ci-install.bash b/ci/ci-install.bash index e889e40fe..2f54e3b3c 100755 --- a/ci/ci-install.bash +++ b/ci/ci-install.bash @@ -37,6 +37,13 @@ else fatal "Unknown os: '$CI_OS_NAME'" fi +if [ "$CI_OS_NAME" = "linux" ]; then + # Avoid slow "processing triggers for man db" + echo "path-exclude /usr/share/doc/*" | sudo tee -a /etc/dpkg/dpkg.cfg.d/01_nodoc + echo "path-exclude /usr/share/man/*" | sudo tee -a /etc/dpkg/dpkg.cfg.d/01_nodoc + echo "path-exclude /usr/share/info/*" | sudo tee -a /etc/dpkg/dpkg.cfg.d/01_nodoc +fi + install-vcddiff() { TMP_DIR="$(mktemp -d)" git clone https://github.com/veripool/vcddiff "$TMP_DIR"