Jenkinsfile: avoid creating agenst when not needed (#405)

runtimeverification · Jul 23, 2019 · 1c4d9d8 · 1c4d9d8
1 parent c9f87f7
commit 1c4d9d8
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -5,15 +5,21 @@ pipeline {
   }
   stages {
     stage("Init title") {
-      when { changeRequest() }
+      when {
+        changeRequest() 
+        beforeAgent true
+      }
       steps {
         script {
           currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}"
         }
       }
     }
     stage('Build and Test') {
-      when { changeRequest() }
+      when {
+        changeRequest()
+        beforeAgent true
+      }
       agent {
         dockerfile {
           additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'