[syslinux] 32bit OS on 64bit architectures

[H. Peter Anvin]

Basically it is not possible to sanely boot a 32-bit kernel with a
64-bit EFI; the opposite is supported, however.

Why would you run a 32-bit kernel these days, though?

	-hpa