On Thu, Sep 17, 2020 at 9:05 AM alciregi@posteo.net wrote:
On Thu, 2020-09-17 at 08:49 -0600, Chris Murphy wrote:
I'm not sure how Boot Options works, i.e. what exactly is it modifying?
Can you try sudo grub2-editenv - set menu_show_once=1
And reboot. Does the GRUB menu appear? If not, then this is likely a
Yes, in this case the GRUB menu appears.
I suggest filing a bug against gnome-shell and report all of this info.