diff --git a/Jenkinsfile b/Jenkinsfile index 7fc6f0a..a05f07f 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -31,19 +31,22 @@ echo "Use settings file at ${maven_settings_file}" echo "Use local repo at ${maven_local_repo_path}" pipeline { + // see https://jenkins.io/doc/book/pipeline/syntax/#agent agent any - // environment variables available to the Pipeline + // see https://jenkins.io/doc/book/pipeline/syntax/#environment environment { JOB_OPTIONS = "${options}" } + // see https://jenkins.io/doc/book/pipeline/syntax/#parameters parameters { choice(choices: ['SNAPSHOT-DRY-RUN', 'SNAPSHOT', 'RELEASE-DRY-RUN', 'RELEASE'], description: 'The type of artifacts the build is expected to generate', name: 'Type') } + //see https://jenkins.io/doc/book/pipeline/syntax/#stages stages { stage('clean up before starting') { script {