On Fri, 4 Jan 2019, Martin Jansa wrote: > On Mon, Dec 17, 2018 at 09:49:16PM +0000, Joseph Myers wrote: > > This patch is OK. > > Hi, > > if it's ok, can you please merge it? Done. -- Joseph S. Myers joseph@codesourcery.com