Editing grub boot menu, how to save?

[Ralf Mardorf]

On Sun, 31 Oct 2021 17:04:08 +0100, Ralf Mardorf wrote:
>IOW the file might never get updated
...

..._if_ it was edited. Updates probably only affect the file _if_ it is
not an edited file.

Again! By one way or the other it is wrong to edit this file to
configure the GRUB menu.

It doesn't matter if Colin is right or my guess should be correct, this
file is not a GRUB config file and editing this file has got
consequences that are unwanted.