--- /dev/null
+* menu.html : the menu used by ../index.html.in and ../index-no-frame
+* home.html : the home page used by ../index.html.in and ../index-no-frame
+* install.html : install instructions
+* download.html : download instructions (obsolete)