(And I agree that we ought to have something for this kind of thing that's easier than editing /etc/grub.d/10_linux, although it will take some careful design work.)
-- No appropriate method for modifying specfic menuentry https://bugs.launchpad.net/bugs/538884 You received this bug notification because you are a member of Ubuntu Bugs, which is subscribed to Ubuntu. -- ubuntu-bugs mailing list ubuntu-bugs@lists.ubuntu.com https://lists.ubuntu.com/mailman/listinfo/ubuntu-bugs
