diff --git a/Jenkinsfile b/Jenkinsfile index 7ab9efd3..4f293248 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -1,5 +1,5 @@ pipeline { - agent any + agent { label "linux || macosx || bsd || solaris || posix || windows" } parameters { // Use DEFAULT_DEPLOY_BRANCH_PATTERN and DEFAULT_DEPLOY_JOB_NAME if // defined in this jenkins setup -- in Jenkins Management Web-GUI