On Fri, 8 Jul 2016, Maciej W. Rozycki wrote: > Any questions or comments before I commit this change? I'll proceed > unless I hear any objections by the end of Monday 11th. I haven't heard back, so I have applied this change now. Maciej