> How did that happen? It's fixed now. Thanks for telling us. No idea. I checked in a fix to doc/web/index.html.