Re: [SeaBIOS] [PATCH 0/6] Convert AHCI driver to run entirely in 32bit mode