diff --git a/.ci/docs.jenkinsfile b/.ci/docs.jenkinsfile index 7d6ff8ec..5f5904e7 100644 --- a/.ci/docs.jenkinsfile +++ b/.ci/docs.jenkinsfile @@ -1,12 +1,12 @@ pipeline { - agent { - dockerfile { filename '.ci/ubuntu18.04.dockerfile' } - } - stages { - stage('Build') { - steps { - sh 'make -C Documentation html SPHINXOPTS="-W"' - } - } + agent { + dockerfile { filename '.ci/ubuntu18.04.dockerfile' } + } + stages { + stage('build') { + steps { + sh 'make -C Documentation html SPHINXOPTS="-W"' + } } + } }