On Thu, 9 Jul 2020 at 16:50, Alex Bennée <[email protected]> wrote: > That looks more like it got missed in a clean-up series because we don't > have coverage in our typical builds and CI?
Yes, very likely. But there's no point in fixing and then adding CI for a config that our users have demonstrated that they do not use; better to just remove it. thanks -- PMM
