diff --git a/contrib/ci/Jenkinsfile b/contrib/ci/Jenkinsfile index 01ae4e08..5ecbe203 100644 --- a/contrib/ci/Jenkinsfile +++ b/contrib/ci/Jenkinsfile @@ -13,7 +13,7 @@ pipeline { } stage('docs') { steps { - sh' make -C docs html' + sh 'make -C docs html' } } stage('build') {