Peter Maydell <[email protected]> writes:
> 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. Fair enough. It can always be restored from the history if someone cares. -- Alex Bennée
