On Tue, 27 Jul 2010, Benjamin Kosnik wrote: >> 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.
Cool. >> 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). > OK Done, also updated on gcc.gnu.org, and removed all .gz files from onlinedocs/libstdc++ (verifying that old had naked .html versions as well). Gerald
