Remove unneeded div.separator from admin menu

[michalzuber]

I was researching the
/* @todo: is this even needed given that it's nested beneath the above li.wp-menu-separator? */

wordpress-svn$ grep -r 'div.*class=".*separator' src |head
src/wp-admin/menu-header.php:110:   echo '<div class="separator"></div>';

Is it necessary to have

#adminmenu div.separator {
    height: 2px;
    padding: 0;
}

The parent <li> has bigger height than that <div>, it is lost there

#adminmenu li.wp-menu-separator {
    height: 5px;
    padding: 0;
    margin: 0 0 6px 0;
    cursor: inherit;
}

[michalzuber]

Related #24104 ?

[helen]

Duplicate of #26960.

[michalzuber]

Replying to helen:

Duplicate of #26960.

Is there a way I can help with that? Where should I report these?
The patch should fix it.
I'm going over the @TODOs in the code.

[helen]

Replying to michalzuber:

I'm going over the @TODOs in the code.

I put the CSS todos in there myself in 3.9. I would like to not focus on that right now - working on an overall roadmap to be published after 4.0, or possibly shortly before release. I appreciate you looking at them, and it is good to know who may be interested in moving forward in general. As for the admin menu in general, it needs a good look at the totality of the markup and CSS. My ticket description and azaozz's comment should give you a good idea of where our thoughts are there.

[michalzuber]

Thanks helen for clarification, appreciate it.