On Sun, 21 Jan 2018, Oleg Endo wrote: > Somehow I never managed to commit the attached patch. > Better late than never. Indeed! (And it looks nice, by the way.) Gerald PS: This is one reason why I usually recommend to add changes as things make it into the tree, not wait until the end of stage 3.