Fix bug #2975 with insufficient docs of texinfo-master-menu.