Merge branch 'master' into latest

kframework · Sep 30, 2019 · 62517c5 · 62517c5
2 parents e646f0c + 5a3b266
commit 62517c5
Showing 1 changed file with 0 additions and 10 deletions.
diff --git 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')