On Sat, 8 Aug 2020, Andreas Tille wrote: > Thanks a lot. BTW, I'd consider it more straightforward if you'd commit > such kind of fixes to Git since it would give you the credit in git log. > I'm also perfectly fine if someone else then me would do a team upload > once there was a successful build.
I can do that now if you want. But for the patch, actually, mailing multiple of them to the list was what led to the final “better” one, so… perhaps this is still good? bye, //mirabilos -- tarent solutions GmbH Rochusstraße 2-4, D-53123 Bonn • http://www.tarent.de/ Tel: +49 228 54881-393 • Fax: +49 228 54881-235 HRB 5168 (AG Bonn) • USt-ID (VAT): DE122264941 Geschäftsführer: Dr. Stefan Barth, Kai Ebenrett, Boris Esser, Alexander Steeg