Merge branch 'master' into latest

Author: chathhorn

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