On Fri, 2014-07-18 at 17:54 +0200, Jakub Jelinek wrote: > On Fri, Jul 18, 2014 at 11:38:22AM -0400, David Edelsohn wrote: > > This is okay with me if it is okay with the Release Managers. > > Ok.
Ok, I committed this as revision 212898. Thanks! Peter
