TODO:

  * Replace "name" attributes with "id" ones in about.html.  "name" is obsolete.
    Note that this may affect the stylesheet.