doc/web/homepage/page-menu.inc


1
2
3
4
5
6
7
8
9
10
11
12
13

    <div class="menu">
      <?php
	 $delim = false;
	 foreach ($menu->urls as $url => $name) {
		 if ($delim) {
			 echo " |\n";
		 }
		 echo "<a href=\"$url\">$name</a>";
		 $delim = true;
	 }
	echo "\n";
	?>
    </div>