[ipxe-devel] ifcpu64.c32

[Sven Dreyer]

Hi List,

does anybody know how to use ifcpu64.c32 from within iPXE?

Documentation of ifcpu64.c32 says that syntax is like this:
ifcpu64.c32 debian64 -- debian32

"debian64" is the menu label to jump to in case of 64-bit CPU 
capability, "debian32" is the label to jump to in other cases.

Unfortunately, I only get:
debian64: command not found

I double-checked that a label named "debian64" does exist in the 
menu.cfg which I'm calling ifcpu64.c32 from. I also tried iPXE script 
URLs instead of menu labels, but with the same results.

Thanks,
Sven