https://gcc.gnu.org/bugzilla/show_bug.cgi?id=87050

--- Comment #9 from Gerald Pfeifer <gerald at pfeifer dot com> ---
(In reply to jos...@codesourcery.com from comment #6)
> A replacement for MetaHTML is already available, we just need to switch to 
> using it.
> 
> https://gcc.gnu.org/ml/gcc-patches/2018-06/msg00176.html

So, I took this report as nudge to speed up completing the transition
from XHTML to HTML 5 that I started earlier this year and expect to be
complete (short of, perhaps, our main page) by next weekend.

That should, as a side effect, allow making David's nice script even a
bit simpler. :-)

Reply via email to