On Fri, Sep 28, 2018 at 6:33 AM Andrew Stubbs <ams@codesourcery.com> wrote: > > On 28/09/18 09:11, Richard Sandiford wrote: > > Yes, thanks. > > Committed. > > Thanks for all the reviews. :-) > This caused: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=89445 -- H.J.