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