diff --git a/Jenkinsfile b/Jenkinsfile index 9c9f1db..b8f39c6 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -3,6 +3,7 @@ pipeline { parameters { booleanParam(defaultValue: true, description: 'Enabled/disables the building of an optimized build', name: 'build_optimized') + booleanParam(defaultValue: true, description: 'Build the libraries as well', name: 'build_libraries') } stages { @@ -75,6 +76,10 @@ pipeline { stages { stage ('Initialize libraries') { + when { + expression { params.build_libraries } + } + steps { sh 'apt-get update' sh 'git reset --hard origin/master; git submodule update --init --remote --recursive --force'