[Dune-devel] Trouble with the CI system

[Oliver Sander]

> that’s really weird, it only happens on this particular MR. I’ve looked into the server logs,
> but nothing really stands out to me. Can you maybe try pushing another change to the
> branch, maybe that will sort it out?

Thanks for looking.  Simply pushing another commit seems to have done the trick.

Best,
Oliver

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <https://lists.dune-project.org/pipermail/dune-devel/attachments/20180815/0237f229/attachment.sig>