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