ci: use the microbenchmarks-pool (#1581)

v1v · web-flow · commit b545f71827dc · 2022-07-08T10:26:23.000+01:00
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -202,7 +202,7 @@ pipeline {
           }
         }
         stage('Benchmarks') {
-          agent { label 'metal' }
+          agent { label 'microbenchmarks-pool' }
           options { skipDefaultCheckout() }
           environment {
             AGENT_WORKDIR = "${env.WORKSPACE}/${env.BUILD_NUMBER}/${env.BASE_DIR}"

Original file line number	Diff line number	Diff line change
`@@ -202,7 +202,7 @@ pipeline {`
`202`	`202`	`}`
`203`	`203`	`}`
`204`	`204`	`stage('Benchmarks') {`
`205`		`- agent { label 'metal' }`
	`205`	`+ agent { label 'microbenchmarks-pool' }`
`206`	`206`	`options { skipDefaultCheckout() }`
`207`	`207`	`environment {`
`208`	`208`	`AGENT_WORKDIR = "${env.WORKSPACE}/${env.BUILD_NUMBER}/${env.BASE_DIR}"`