$tmp_buff .= ' <li><a href="publis.html"><span>Publications</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="people.html"><span>People</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="history.html"><span>History</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="contrib.html"><span>Contrib</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="publis.html"><span>Publications</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="people.html"><span>People</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="history.html"><span>History</span></a></li>'."\n";
$tmp_buff .= ' <li><a href="contrib.html"><span>Contrib</span></a></li>'."\n";