changing default grub entry??

[Tom H]

On Sat, Oct 13, 2018 at 1:51 AM Ralf Mardorf via ubuntu-users
<ubuntu-users at lists.ubuntu.com> wrote:
> On Fri, 12 Oct 2018 15:45:19 +0200, Tom H wrote:
>>
>> In addition to the weird counting that I showed in my first reply, you
>> can also avoid "saved" and set GRUB_DEFAULT using the title or the
>> menuentry_id_option:
>
> https://lists.ubuntu.com/archives/ubuntu-users/2018-October/295498.html
>
> https://www.gnu.org/software/grub/manual/grub/grub.html

Thanks