Ticket #40927: plugin.diff

plugin.php

@@ -1098 +1098 @@
         } elseif ( isset( $menu[ "$position" ] ) ) {
                 $position = $position + substr( base_convert( md5( $menu_slug . $menu_title ), 16, 10 ) , -5 ) * 0.00001;
                 $menu[ "$position" ] = $new_menu;
+        } elseif ( 'double' === gettype( $position ) ) {
+                $menu[ (string)$position ] = $new_menu;
         } else {
                 $menu[ $position ] = $new_menu;
         }