Hi!
On Mon Sep 23, 2002 at 01:06:56 +0000, Alexey Mandrookin wrote:
I found strange behaviour of l4_i386_ipc_wait(). In case of interrupt IPC, it return wrong value of the thread id of IPC source.
You're waiting for a specific interrupt, how useful it is to know the "source" if you already have the dest id (this specific interrupt)?
If you're waiting for an interrupt, use ipc_receive, don't care about source stuff (also see p. 29 of the L4-V2 ref manual).
Adam