I have forgotten... Compilation is done with :
gcc -nostdinc -I/home/bertrand/openvms/l4/gcc-4.7/include
-I/home/bertrand/openvms/l4/pistachio/kernel/src
-I/home/bertrand/openvms/l4/pistachio/kernel/src/generic
-I/usr/lib/gcc/x86_64-linux-gnu/4.7/include/ -Ux64 -Ux86 -Uk8 -Upc99
-Uv4 -Uhs -D__SUBARCH__=x64 -D__ARCH__=x86 -D__CPU__=k8
-D__PLATFORM__=pc99 -D__API__=v4 -D__SCHED__=hs -imacros
/home/bertrand/openvms/l4/gcc-4.7/config/config.h -imacros
/home/bertrand/openvms/l4/pistachio/kernel/src/generic/macros.h -include
/home/bertrand/openvms/l4/pistachio/kernel/src/generic/config.h
-include /home/bertrand/openvms/l4/pistachio/kernel/src/generic/types.h
-fno-rtti -fno-builtin -fomit-frame-pointer -fno-exceptions -Wall
-Wno-non-virtual-dtor -Wno-format -O2 -m64 -mcmodel=kernel -mno-red-zone
-mno-mmx -mno-sse -mno-sse2 -mno-sse3 -march=k8 -Wno-conversion
-fno-stack-protector -c
/home/bertrand/openvms/l4/pistachio/kernel/src/glue/v4-x86/idt.cc