diff --git a/Jenkinsfile b/Jenkinsfile index 7a0d8dc8c..b50df6ea0 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -1,5 +1,5 @@ pipeline { - agent {'label JDK_8'} + agent {label 'JDK_8'} options { retry(3) timeout(time: 30, unit: 'MINUTES')