diff --git a/Jenkinsfile2 b/Jenkinsfile2 index fceaa6554faa5bde7ae028ec9204627d505e8b95..0ca51b0366cd66584ed37763070a907558217761 100644 --- a/Jenkinsfile2 +++ b/Jenkinsfile2 @@ -171,6 +171,25 @@ pipeline { ''' } } + stage ('build docs') { + when { + allOf { + changeRequest() + { expression { env.CHANGE_BRANCH =~ /docs\// }} + } + } + agent {label "docusaurus"} + steps { + timeout(time: 5, unit: 'MINUTES') { + sync_source() + script { + sh ''' + echo hello + ''' + } + } + } + } stage ('Parallel build stage') { //only build pr options { skipDefaultCheckout() }