I've now pushed this wwwdocs patch, which Gerald approved at
https://gcc.gnu.org/pipermail/gcc-patches/2021-June/572796.html