Ticket #3783: menu.diff

menu.php

@@ -106 +106 @@
         if ( $ptype_obj->show_in_menu !== true ) {
                 continue;
         }
-        $ptype_menu_position = is_int( $ptype_obj->menu_position ) ? $ptype_obj->menu_position : ++$_wp_last_object_menu; // If we're to use $_wp_last_object_menu, increment it first.
+        $ptype_menu_position = is_numeric( $ptype_obj->menu_position ) ? $ptype_obj->menu_position : ++$_wp_last_object_menu; // If we're to use $_wp_last_object_menu, increment it first.
         $ptype_for_id        = sanitize_html_class( $ptype );
 
         $menu_icon = 'dashicons-admin-post';