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 c2b78f390a13593b62364bc722cdc6d60f786546..e3068a5a11c35c60b5445893f47d3413aa4a7ce9 100644 (file)
--- 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'
       }
     }
   }