+ $_registered_pages[$hookname] = true;
+ // backwards-compatibility for plugins using add_management page. See wp-admin/admin.php for redirect from edit.php to tools.php
+ if ( 'tools.php' == $parent )
+ $_registered_pages[get_plugin_page_hookname( $file, 'edit.php')] = true;
+