On Tue, Dec 01, 2020 at 08:18:45PM +0100, Martin Ågren wrote: > Seems to me like we can go with a change like this. If you're on a > pre-1.77.1 system and want user-manual.html, but don't want to update > your tool chain, you should still be able to clone the "htmldocs" repo. > I'm not sure exactly where the cut-off point is, but I think moving up > to mid-2012 should be ok. Yeah, I think this is the key thing. We can afford to be a bit more aggressive with the doc toolchain requirements in general because there's an easy fallback. (Though I think even without that, it sounds like this version is pretty safe, and the proposed change would not even break the old versions, but keep them with the same behavior). The overall proposal sounds like a good idea to me, as long as the review comments I saw elsewhere. -Peff
