CI: kill older running builds

diff --git a/Jenkinsfile b/Jenkinsfile
index c2b78f390a13593b62364bc722cdc6d60f786546..2475c22dafbec66e9b06c199abac1d97bc282c1c 100644 (file)
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -1,11 +1,25 @@
 #!groovy
 
+// load library https://github.com/tjhei/jenkins-stuff to provide
+// killold.killOldBuilds() function:
+@Library('tjhei') _
+
 pipeline
 {
   agent none
 
   stages
   {
+    stage("abort old")
+    {
+      agent none
+      steps
+      {
+        // kill older builds in this PR:
+        script { killold.killOldBuilds() }
+      }
+    }
+
     stage("check")
     {
       agent

diff --git a/contrib/ci/Jenkinsfile.osx b/contrib/ci/Jenkinsfile.osx
index 5a404aabb774f3e4442e9c991dbb3978a2a7cf99..68205e5b8bedb785f044504e48cba57752e042f7 100644 (file)
--- a/contrib/ci/Jenkinsfile.osx
+++ b/contrib/ci/Jenkinsfile.osx
@@ -19,8 +19,28 @@ Settings to apply inside Jenkins:
   - discard: 5+ items
 */
 
+// load library https://github.com/tjhei/jenkins-stuff to provide
+// killold.killOldBuilds() function:
+@Library('tjhei') _
+
 pipeline
 {
+  agent none
+
+  stages
+  {
+    stage("abort old")
+    {
+      agent none
+      steps
+      {
+        // kill older builds in this PR:
+        script { killold.killOldBuilds() }
+      }
+    }
+
+    stage("main")
+    {
   agent {
     node {
         label 'osx'
@@ -95,4 +115,6 @@ pipeline
       }
     }
   }
+  }
+  }
 }

diff --git a/contrib/ci/Jenkinsfile.tidy b/contrib/ci/Jenkinsfile.tidy
index 82d7e69a39f2580a7c8958ea4948f1f2a7171f12..80ebb236a8c37d403cff2a8fa5d38f6a978eef38 100644 (file)
--- a/contrib/ci/Jenkinsfile.tidy
+++ b/contrib/ci/Jenkinsfile.tidy
@@ -19,8 +19,30 @@ Settings to apply inside Jenkins:
   - discard: 5+ items
 */
 
+// load library https://github.com/tjhei/jenkins-stuff to provide
+// killold.killOldBuilds() function:
+@Library('tjhei') _
+
 pipeline
 {
+  agent none
+
+  stages
+  {
+    stage("abort old")
+    {
+      agent none
+      steps
+      {
+        githubNotify context: 'tidy', description: 'initializing...',  status: 'PENDING'
+        // kill older builds in this PR:
+        script { killold.killOldBuilds() }
+      }
+    }
+
+    stage("main")
+    {
+
   agent
   {
     docker
@@ -88,4 +110,6 @@ pipeline
     }
 
   }
+  }
+  }
 }