ed5db5831e
MACHINE. Thus, move it out of <arm/bootconfig.h> and put it into <machine/bootconfig.h> on those MACHINEs (cats, hpcarm, and shark) where it's used outside the file in which it's defined.