[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#44027: [PATCH] installer: Create bios_grub partition when it is need
From: |
Miguel Ángel Arruga Vivas |
Subject: |
bug#44027: [PATCH] installer: Create bios_grub partition when it is needed. |
Date: |
Mon, 19 Oct 2020 21:59:30 +0200 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) |
Hi,
Mathieu Othacehe <othacehe@gnu.org> writes:
> Hello Miguel,
>
>> Is there any other issue remaining? It doesn't modify this logic at
>> all. Should I apply this patch to master then?
>
> Yes, your patch LGTM. Please make sure that system tests are still
> working by running:
>
> make check-system TESTS="gui-installed-os gui-installed-os-encrypted
> gui-installed-desktop-os-encrypted"
I pushed it to master as 19c14d95b3 after running successfully these
system tests.
Thank you very much, and happy hacking!
Miguel
signature.asc
Description: PGP signature
- bug#44027: 1.2-29a2eb3 Installer fails at final stage installing GRUB., (continued)
- bug#44027: 1.2-29a2eb3 Installer fails at final stage installing GRUB., Brett Gilio, 2020/10/16
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Miguel Ángel Arruga Vivas, 2020/10/17
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Brendan Tildesley, 2020/10/17
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Brendan Tildesley, 2020/10/18
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Miguel Ángel Arruga Vivas, 2020/10/18
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Mathieu Othacehe, 2020/10/18
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Brendan Tildesley, 2020/10/19
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Mathieu Othacehe, 2020/10/19
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Miguel Ángel Arruga Vivas, 2020/10/19
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Mathieu Othacehe, 2020/10/19
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed.,
Miguel Ángel Arruga Vivas <=
- bug#44027: [PATCH] installer: Create bios_grub partition when it is needed., Bengt Richter, 2020/10/20