You could, most likely, enter it by hand into the grub configuration; & it should then be available on your next reboot.
In /boot/grub/grub.cfg; ### BEGIN /etc/grub.d/40_custom ### # This file provides an easy way to add custom menu entries. Simply type the # menu entries you want to add after this comment. Be careful not to change # the 'exec tail' line above. ### END /etc/grub.d/40_custom ### -- Sent from FOSS (Free Open Source Software) Debian GNU/Linux -- To UNSUBSCRIBE, email to debian-user-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/CAL36VGkt6XfXYxR=hhzo-tfcxpkgn3xvnr93mcpdkm6u-lo...@mail.gmail.com
