From: Daniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Date: Thu, 28 Mar 2019 00:28:19 +0000 (-0400)
Subject: Merge pull request #7868 from tjhei/jenkins_status_end
X-Git-Tag: v9.1.0-rc1~241
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9344ce220a1497b7bc40f1787098d80edfc1cc3f;p=dealii.git

Merge pull request #7868 from tjhei/jenkins_status_end

CI: fix left-over "pending"
---

9344ce220a1497b7bc40f1787098d80edfc1cc3f