From: Timo Heister <timo.heister@gmail.com>
Date: Sun, 24 Mar 2019 23:40:20 +0000 (-0600)
Subject: CI: kill older running builds
X-Git-Tag: v9.1.0-rc1~238^2~1
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a5577ea660d98051e9c8d682485f9749e85b2a8d;p=dealii.git

CI: kill older running builds
---

diff --git a/Jenkinsfile b/Jenkinsfile
index c2b78f390a..2475c22daf 100644
--- 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 5a404aabb7..68205e5b8b 100644
--- 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 82d7e69a39..80ebb236a8 100644
--- 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
     }
 
   }
+  }
+  }
 }