Double encoded Menu TItles

If a menu item is entered with an ampersand (e.g. "Help & Resources") it displays as "Help & Resources".

line 22 of includes/menu.inc is

$title = check_plain($elem['#title']);

later, the $title is run through l() which will check_plain() that title again.

line 62

$out .= l($title, $elem['#href'], $options);