Compiling L4Ka::Pistachio with SMP support

I had no problems cloning the Pistachio repository and compiling the
default kernel, but I'm having an issue whenever I enable SMP support
in the kernel.  The specific error is in interrupt.cc with an
undeclared 'is_pending'.

/home/jnwhiteh/l4ka-pistachio/kernel/src/api/v4/interrupt.cc: In function `void
   migrate_interrupt_end(tcb_t*)':
/home/jnwhiteh/l4ka-pistachio/kernel/src/api/v4/interrupt.cc:411: error: `
   is_pending' undeclared (first use this function)
/home/jnwhiteh/l4ka-pistachio/kernel/src/api/v4/interrupt.cc:411: error: (Each
   undeclared identifier is reported only once for each function it appears
   in.)
make[1]: *** [src/api/v4/interrupt.o] Error 1
make[1]: Leaving directory `/home/jnwhiteh/l4ka-pistachio/x86-kernel-build'
make: *** [all] Error 2

The full compile log can be found at http://l4ka.pastey.net/106311.
Has anyone run into this error or is there a known fix for the issue?

Jim Whitehead
University of Oxford
Computing Laboratory