Jenkinsfile: use node instead of stage

runtimeverification · Jun 11, 2019 · 2fb7ca5 · 2fb7ca5
1 parent 5ccc693
commit 2fb7ca5
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -3,9 +3,8 @@ pipeline {
     ansiColor('xterm')
   }
   stages {
-    stage('Kill old builds') {
-      agent any
-      steps {
+    node {
+      stage('Kill old builds') {
         build.getProject()._getRuns().iterator().each{ run ->
           def exec = run.getExecutor()
           //if the run is not a current build and it has executor (running) then stop it