php/web/

PHP scripts for the web.

nav.php

Creates the navigation boxes on the left of every page.

readme.php

Collects information about source code directories from Abstract, Readme, Links files, and formats it for HTML output.