On 13.03.19 21:09, Richard Levitte wrote: > > So yeah, we do need to remember that PRs go through the CIs before > merging. > Agreed, and thanks Rich for the polite reminder :-) Matthias