Hi Michael, sorry about the delay. I swear I had this working before, but now the new test isn't passing. Because this is just a clean-up change that doesn't actually fix anything, I don't want to put any more effort into it. Feel free to try and salvage the patch or to trash it.
On Sun, Oct 18, 2020 at 10:13 AM Michael Albinus <[email protected]> wrote: > > Hi Nicholas, > > Are you still working on this? > > Best regards, Michael.
