[tde-users] GRUB menu issue

This came up in conversation here a few days ago -- I was the one asking -- and there being a solution I thought I'd post it here. For reasons unknown, and that make no sense to me, the GRUB menu is not enabled by default in Ubuntu 20,04 and perhaps closely related distributions. To get it back, it's necessary to edit the default /etc/default/grub, changing GRUB_TIMEOUT_STYLE='hidden" to GRUB_TIMEOUT_STYLE="menu" and uncommenting GRUB_TERMINAL="console" and after that the GRUB menu is back at boot. -- dep Pictures: http://www.ipernity.com/doc/depscribe/album Column: https://ofb.biz/author/dep/