https://gcc.gnu.org/bugzilla/show_bug.cgi?id=122638
--- Comment #15 from ro at CeBiTec dot Uni-Bielefeld.DE <ro at CeBiTec dot Uni-Bielefeld.DE> --- > --- Comment #14 from Gerald Pfeifer <gerald at pfeifer dot com> --- > (In reply to [email protected] from comment #13) >> My primary point is that right now you're worse off if you have a >> version of makeinfo too old to build current docs than without makeinfo >> at all. When it's acceptable not to build info docs when makeinfo is >> missing completely, it should just be as acceptable not to build them >> whenever it's considered too old. > > I agree. > > Let's go for that. Would you like to propose a patch? I'd rather leave this to Eric: he's already digged out the necessary autoconf support to do so, and I've got too much on my plate already.
