]> https://gitweb.dealii.org/ - dealii.git/commitdiff
CI: fix left-over "pending" 7868/head
authorTimo Heister <timo.heister@gmail.com>
Wed, 27 Mar 2019 15:31:23 +0000 (09:31 -0600)
committerTimo Heister <timo.heister@gmail.com>
Wed, 27 Mar 2019 15:31:23 +0000 (09:31 -0600)
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...

Jenkinsfile

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

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.