https://gcc.gnu.org/bugzilla/show_bug.cgi?id=87449
--- Comment #3 from Martin Diehl <m.diehl at mpie dot de> --- Dear Dominique, sorry for the duplicated reports, I always got an server error and assumed filing the report failed. best regards, Martin On Fri, 2018-09-28 at 17:06 +0000, dominiq at lps dot ens.fr wrote: > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=87449 > > --- Comment #2 from Dominique d'Humieres <dominiq at lps dot ens.fr> > --- > *** Bug 87459 has been marked as a duplicate of this bug. *** >