diff --git a/Jenkinsfile b/Jenkinsfile index ae580b383db8156d2b0c5608d58ff398649ce955..d000ddcc0b084f3eec937c45c12d3000cacd01f4 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -380,7 +380,7 @@ pipeline { } } build { target = 'check-header' } - build { } + build { target = 'all' } } } }