From 5a3b266fa527995a5f6ffe81f2bf38530021ee04 Mon Sep 17 00:00:00 2001
From: Chris Hathhorn <chathhorn@gmail.com>
Date: Mon, 30 Sep 2019 10:39:40 -0500
Subject: [PATCH] Disable pushing docker images to internal registry. (#583)

---
 Jenkinsfile | 10 ----------
 1 file changed, 10 deletions(-)

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')