try to reuse node for docker container (runtimeverification#281)

dwightguth · web-flow · commit 92b5a3ace3c0 · 2019-01-31T16:23:13.000-06:00
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -67,6 +67,7 @@ pipeline {
         docker {
           image 'ubuntu:bionic'
           args '-u 0'
+          reuseNode true
         }
       }
       options { skipDefaultCheckout() }

Original file line number	Diff line number	Diff line change
`@@ -67,6 +67,7 @@ pipeline {`
`67`	`67`	`docker {`
`68`	`68`	`image 'ubuntu:bionic'`
`69`	`69`	`args '-u 0'`
	`70`	`+ reuseNode true`
`70`	`71`	`}`
`71`	`72`	`}`
`72`	`73`	`options { skipDefaultCheckout() }`