luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

ci: avoid man page builds (#6398)

This commit is contained in:
Wilson Snyder 2025-09-06 18:48:39 -04:00 committed by GitHub
parent 46f8003c4e
commit d186dcdc32
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
ci/ci-install.bash
View File

@ -37,6 +37,13 @@ else
fatal "Unknown os: '$CI_OS_NAME'" fatal "Unknown os: '$CI_OS_NAME'"
fi 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() { install-vcddiff() {
TMP_DIR="$(mktemp -d)" TMP_DIR="$(mktemp -d)"
git clone https://github.com/veripool/vcddiff "$TMP_DIR" git clone https://github.com/veripool/vcddiff "$TMP_DIR"