The css class for the "Jump" box in print_menu() in html_api.php originally had class="right", which leaves some odd whitespace around the box, and it doesn't look like it belongs to the rest of the menu (look at the "Jump" box here on the upper-right to see what I mean).

Changing that class to "jumpright" in html_api.php fixes it:

PRINT '<td class="jumpright" style="white-space: nowrap;">';