'."\n";
$r.='';
$r.=''."\n";
$r.=''."\n";
$r.=''."\n";
$r.='Projects';
$r.=' | '."\n";
$r.=' '."\n";
$r.=' ';
$r.=' | ';
$r.='';
$r.=''."\n";
$r.=''."\n";
my @platforms=@platforms;
while (@platforms) {
my $platform_sym =shift @platforms;
my $platform_name=shift @platforms;
my $chosen=($platform_selected && $platform_selected eq $platform_sym);
$r.='';
$r.=a_href((!$platform_selected ? "" : "/project/").'#'.$platform_sym,$platform_name,
"attr"=>($chosen
? 'style="text-decoration: underline; font-weight: bold;"'
: 'style="text-decoration: inherit; /* revoke underline */"'));
$r.=" | \n";
}
$r.=' '."\n";
$r.=' '."\n";
$r.=' | '."\n";
$r.='