> gcc.gnu.org will be preferrable, I think. That allows a number of us > to help out if neede, re-running scripts, etc. Right. The Makefiles are set up for this now. > For the time being I suggest to apply the patch below, though. What > we have in place as of today simply is broken (and has been for > quarters, at a minimum). > > Objections? OK -benjamin