On 2024-07-22 17:30:18 +0200, Vincent Lefevre wrote:
> After a recent grub2 upgrade, there are now duplicate "GNU/Linux"
> in menuentry and submenu lines of /boot/grub/grub.cfg, e.g.
>
> menuentry 'Debian GNU/Linux GNU/Linux' --class debian --class gnu-linux
> --class gnu --class os $menuentry_id_option
> 'gnulinux-simple-f3a51d21-c3a1-405d-b0fb-b0b25662b752' {
>
> submenu 'Advanced options for Debian GNU/Linux GNU/Linux'
> $menuentry_id_option 'gnulinux-advanced-f3a51d21-c3a1-405d-b0fb-b0b25662b752'
> {
I think that this is because in /etc/default/grub, the
GRUB_DISTRIBUTOR line got changed to
GRUB_DISTRIBUTOR=`( . /etc/os-release; echo ${NAME:-Debian} ) 2>/dev/null ||
echo Debian`
One should normally get "Debian", but /etc/os-release contains
NAME="Debian GNU/Linux"
instead of just
NAME="Debian"
--
Vincent Lefèvre <[email protected]> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
