[chore] Rename 'More plugins' to 'More tools'

More tools is a submenu in the tools menu, not in the plugins menu. That everything in there happens to be plugins is merely a technical detail and not considered part of the unifying menu vision. Plugin management should be last as it is because it's only used once in a blue moon, if it should be in the tools menu at all. The same applies to settings more broadly. Putting plugin management in the tools menu is traditional, however.

Plugins should not and are not supposed to be most at home in the tools menu. Those plugins that happen to be in the tools menu are by and large there because that's where they fit best. Those that don't are new and I didn't have the heart or energy to make much of a fuzz about it provided they had a reasonable claim to the tools menu. That includes plugins like tweak document settings which should be more at home in settings → document.

Also see <koreader#6105 (comment)>.

frontend/ui/elements/common_info_menu_table.lua

@@ -26,7 +26,7 @@ common_info.help = {
     text = _("Help"),
 }
 common_info.more_plugins = {
-    text = _("More plugins"),
+    text = _("More tools"),
 }
 
 common_info.device = {