Re: [SeaBIOS] [PATCH v2 02/22] virtio: run drivers in 32bit mode