diff --git a/Jenkinsfile b/Jenkinsfile index 24d8b8cd8..97d6576d9 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -1,9 +1,6 @@ // Object holding the docker image. def img -// Our internal registry. -def PRIVATE_REGISTRY = "https://10.0.0.21:5201" - pipeline { agent none options { @@ -27,13 +24,6 @@ pipeline { img = docker.build "c-semantics:${env.CHANGE_ID}" } } } - stage ( 'Push to private registry' ) { steps { - script { - docker.withRegistry ( "${PRIVATE_REGISTRY}", 'rvdockerhub' ) { - img.push() - } - } - } } stage ( 'Compile' ) { options { timeout(time: 70, unit: 'MINUTES')