Building a 32-bit kernel on a 64-bit host...