COMMUNITY-81: update dockerfile name

ManuelJNunez · ManuelJNunez · commit dfd1502f5b48 · 2024-02-16T11:58:41.000+01:00
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -51,7 +51,7 @@ pipeline {
         stage('Build sequence') {
             agent {
                 dockerfile {
-                    filename 'resources/docker/Dockerfile.x64Linux4gcc7.3.0'
+                    filename 'resources/docker/Dockerfile.linux'
                     label 'docker'
                 }
             }

Original file line number	Diff line number	Diff line change
`@@ -51,7 +51,7 @@ pipeline {`
`51`	`51`	`stage('Build sequence') {`
`52`	`52`	`agent {`
`53`	`53`	`dockerfile {`
`54`		`- filename 'resources/docker/Dockerfile.x64Linux4gcc7.3.0'`
	`54`	`+ filename 'resources/docker/Dockerfile.linux'`
`55`	`55`	`label 'docker'`
`56`	`56`	`}`
`57`	`57`	`}`