From: Timo Heister <timo.heister@gmail.com>
Date: Wed, 27 Mar 2019 15:31:23 +0000 (-0600)
Subject: CI: fix left-over "pending"
X-Git-Tag: v9.1.0-rc1~241^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fpull%2F7868%2Fhead;p=dealii.git

CI: fix left-over "pending"

If the CI jenkins job ends up starting quicker than the .mark step, we
are left with a "pending" github status. Fix this by setting it to green
a second time. It is unlikely that the mark step is slower than the
whole CI run...
---

diff --git a/Jenkinsfile b/Jenkinsfile
index c2b78f390a..e3068a5a11 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -183,6 +183,8 @@ pipeline
       steps
       {
         githubNotify context: 'CI', description: 'OK',  status: 'SUCCESS'
+        // In case the Jenkinsfile.mark job started after we did, make sure we don't leave a pending status around:
+        githubNotify context: 'ready', description: ':-)',  status: 'SUCCESS'
       }
     }
   }