https://gcc.gnu.org/bugzilla/show_bug.cgi?id=78293
--- Comment #11 from paul.richard.thomas at gmail dot com <paul.richard.thomas at gmail dot com> --- I rather suspect that was why I had deleted the tree :-) That's a pity. I am afraid moving from one country to another caused this PR to get lost. Cheers Paul On 1 November 2017 at 18:18, dominiq at lps dot ens.fr <gcc-bugzi...@gcc.gnu.org> wrote: > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=78293 > > --- Comment #10 from Dominique d'Humieres <dominiq at lps dot ens.fr> --- >> Dominique, >> >> Do you still have 5-branch and, if so, could you commit the patch to it >> please? >> >> Cheers >> >> Paul > > Paul, > > The 5-branch is now closed. > > Dominique > > -- > You are receiving this mail because: > You are on the CC list for the bug. > You are the assignee for the bug.
