diff --git a/Jenkinsfile b/Jenkinsfile index 030f4ef..a33822c 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -38,7 +38,10 @@ pipeline { description: 'The location of the local repository') string(name: 'exec_label', defaultValue: 'CI', - description: 'Run on all nodes matching the label') + description: 'Run on all nodes matching the label') + string(name: 'build_options', + defaultValue: '', + description: 'Additional options for Maven.') } agent {