| // +--------------------------------------------------------------------+ // // $Id: default-menu-header.php 13 2003-02-23 04:12:48Z luca $ // /** * Draws the menu header. */ ?>