Re: Language menu in the HTML manual

[Andreas Enge]

Am Mon, Jan 24, 2022 at 04:11:16PM +0100 schrieb Ludovic Courtès:
> Heh.  :-)  Done!  That should appear on-line soon (you may have to
> reload with Ctrl-F5.)

Thanks, working well! (Except for the sun that has disappeared again...)

Andreas