<!-- $Id$ -->
<?php

   echo "Dump HTML called.<p>\n";
   echo "Got: $dumpHTML $directory<br>\n";

?>
