Ping? It's a very simple change. On Sat, Aug 6, 2016 at 4:33 PM, Roland McGrath <mcgrathr@google.com> wrote: > A simple omission that was easy to fix. I don't know if this warrants > a NEWS entry or anything. > > > Thanks, > Roland