On Fri, 6 Oct 2017, Thomas Koenig wrote: > I just committed the change below. Gerald's bot had no > complaints, so I guess this must be OK :-)
Yes, and generally when it comes to the web pages, better change than sorry (of missing something). :-) Well, don't break the main page I guess, but, really, having up-to-date and complete contents up is more important than the occasional minor markup error. So, thanks, and keep that up! Gerald
