Remove dependency on Menu module

I do not understand that either.

Completed this patch by adding hook_modules_installed() in order to lazy-add the menu in case Menu module is installed later.

I don't understand what the point of this patch is. Much of the functionality of Devel is in its menu and installing it without menu.module would cripple it. I don't care to see support requests from people who can't find things because they don't have menu.module enabled.

If you install Devel, then I don't see why you'd worry about installing Menu.

Well, there are site concepts that simply don't need Menu module to be installed. Devel module does not require Menu module; it merely exposes a custom menu if it's there. Devel's router paths, local tasks, as well as developer functions are working fine without the menu. And somewhat related, most users of admin_menu usually don't enable Devel's menu block at all, as most of the functionality is exposed in the admin menu already.

IIRC uninstall requires menu

The patch already takes devel_uninstall() into account:

+++ devel.install	26 Jan 2011 01:49:09 -0000
@@ -41,8 +45,11 @@ function devel_uninstall() {
   // Delete the development menu.
-  $devel_menu = menu_load('devel');
-  menu_delete($devel_menu);
+  if (module_exists('menu')) {
+    if ($devel_menu = menu_load('devel')) {
+      menu_delete($devel_menu);
+    }
+  }

and even uses hook_modules_installed() to act if Menu module is installed later on.

Will we get errors if menu module gets disabled and then re-enabled? If not, this looks good to go.

Well, then I'd ask you to remove the dependency from devel_node_access, too, please.

Decided to commit this after some light testing. Pls reopen if there are problems.