commit 2150da8ee59fb2edbb3e90bc53f7baac1601db7d
author Davide Pesavento <davidepesa@gmail.com> Fri Jul 08 18:18:51 2022 -0400
committer Davide Pesavento <davidepesa@gmail.com> Fri Jul 08 18:18:51 2022 -0400
tree 71f0acbcb026648c12c39bb11c199237a98ec207
parent 990620ac3b86cd599098f3fc8392a315999647e7

build+docs: support CentOS Stream 9, drop CentOS 8

Refs: #5181
Change-Id: I2d8bc595bad047ceaa78bd3729848491b843e83d

.jenkins.d/10-build.sh

diff --git a/.jenkins.d/10-build.sh b/.jenkins.d/10-build.sh
index 58c8b06..c514c3a 100755
--- a/.jenkins.d/10-build.sh
+++ b/.jenkins.d/10-build.sh
@@ -10,8 +10,7 @@
 if [[ $JOB_NAME == *"code-coverage" ]]; then
     COVERAGE="--with-coverage"
 fi
-if has CentOS-8 $NODE_LABELS; then
-    # https://bugzilla.redhat.com/show_bug.cgi?id=1721553
+if [[ -n $DISABLE_PCH ]]; then
     PCH="--without-pch"
 fi