On Thu, 17 Mar 2016 12:13:45 +0100, Pedro Alves wrote: > On 03/15/2016 10:07 PM, Jan Kratochvil wrote: > > Is at least this little suggestion OK? > > OK. Checked in: 708bf0a14b10d801a600759f3ef6d272978ae854 Thanks, Jan