]> https://gitweb.dealii.org/ - dealii.git/commitdiff
Merge pull request #7859 from tjhei/ci_abort_old
authorLuca Heltai <luca.heltai@sissa.it>
Thu, 28 Mar 2019 07:52:29 +0000 (08:52 +0100)
committerGitHub <noreply@github.com>
Thu, 28 Mar 2019 07:52:29 +0000 (08:52 +0100)
CI: kill older running builds

1  2 
Jenkinsfile

diff --cc Jenkinsfile
Simple merge

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.