On Saturday, May 23, 2020 2:56:59 AM CDT Graham Inggs wrote: > > This was fixed in an upload done slightly before the bug was filed, though > > with > > a different patch; I'll probably replace it with this one in a subsequent > > upload. > > Great, thank you! Would you like a merge request, or I could even > push directly to salsa, if you prefer? > >
Sure, pushing directly to Salsa is fine, thank you.