Hi Colin, > * /etc/default/grub > * the resulting /boot/grub/grub.cfg > * any output from "sudo update-grub"
Oh .. now I see .. my /etc/default/grub was renamed to /etc/default/grub.ucf-dist and no /etc/default/grub remain. Not sure how that did happen, though. Renaming /etc/default/grub.ucf-dist to /etc/default/grub and running update-grub indeed showed up the correct boot options. Please close the bug or adjust severity accordingly. I don't remember having allowed dpkg to disable my /etc/default/grub (I would have realized that ..) until I rebooted. Thanks and all the best Norbert -- PREINING Norbert https://www.preining.info Accelia Inc. + IFMGA ProGuide + TU Wien + JAIST + TeX Live + Debian Dev GPG: 0x860CDC13 fp: F7D8 A928 26E3 16A1 9FA0 ACF0 6CAC A448 860C DC13
