diff --git a/ci/Jenkinsfile.release b/ci/Jenkinsfile.release index fe24d916b..61404b99d 100644 --- a/ci/Jenkinsfile.release +++ b/ci/Jenkinsfile.release @@ -57,7 +57,7 @@ pipeline { stage('Build') { steps { script { image = docker.build( - "${params.IMAGE_NAME}:${env.GIT_COMMIT.take(8)}", + "${params.IMAGE_NAME}:${params.IMAGE_TAG ?: env.GIT_COMMIT.take(8)}", "--label=commit='${env.GIT_COMMIT.take(8)}' " + "--build-arg=MAKE_TARGET='${params.MAKE_TARGET}' " + "--build-arg=NIMFLAGS='${params.NIMFLAGS}' " + @@ -82,7 +82,10 @@ pipeline { credentialsId: params.DOCKER_CRED, url: "" ]) { image.push() - image.push(env.IMAGE_TAG) + /* If Git ref is a tag push it as Docker tag too. */ + if (params.GIT_REF ==~ /v\d+\.\d+\.\d+.*/) { + image.push(params.GIT_REF) + } } } } }