On Mon, Nov 26, 2018 at 12:42:06PM +0100, Tim Düsterhus wrote: > While cleaning up my local branches I noticed that this patch is not yet > merged and probably slipped through. > > Message-ID: [email protected] > Archive : https://www.mail-archive.com/[email protected]/msg31231.html
Ah indeed, now applied, thank you! Willy

