]> https://gitweb.dealii.org/ - dealii.git/commit
projects / dealii.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cc6929e) | patch
Jenkins: delete mark job as well, as it is not needed anymore 14636/head
authorTimo Heister <timo.heister@gmail.com>
Tue, 3 Jan 2023 19:00:59 +0000 (14:00 -0500)
committerTimo Heister <timo.heister@gmail.com>
Tue, 3 Jan 2023 19:00:59 +0000 (14:00 -0500)
commit82b29cfca93cafc8d3eda957d45d6152fa12f77a
treec9e4a7b02563a25680da02e42c413778674a1999tree | snapshot
parentcc6929e62105b42bf82f1715af9f95fe4d26d903commit | diff
Jenkins: delete mark job as well, as it is not needed anymore

This is because invidual jobs report there status without having to

be on a node yet.
contrib/ci/Jenkinsfile.mark [deleted file] blob | history
Mirror of the development repository for deal.II

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.