On Mon, 21 Dec 2020 16:20:36 -0000 (UTC)
Amadeus WM via users wrote:
looks like
sudo grub2-editenv - unset menu_auto_hide
should disable it.
No doubt it should, but absolutely everything I tried would
not work consistently until I got out the big hammer.
There are 47 million GRUB_xxx settings you can put in
/etc/default/grub, why GRUB_SHOW_ME_THE_MENU isn't one, I
have no idea :-).