diff --git a/libsel4/include/interfaces/sel4.xml b/libsel4/include/interfaces/sel4.xml index c5956d25e..cd9cb04ea 100644 --- a/libsel4/include/interfaces/sel4.xml +++ b/libsel4/include/interfaces/sel4.xml @@ -1369,8 +1369,9 @@ a signal arrives, the passive thread will receive the scheduling context and possess it until it waits on the notification object again. - This operation will fail if the scheduling context is already bound to a thread or - notification object. + This operation will fail for notification objects if the scheduling context is already + bound to a notification object, and for thread objects if the the scheduling context is + already bound to a thread. See @@ -1381,7 +1382,7 @@ The is a CPtr to a capability of the wrong type. - Or, or is already bound. + Or, or is already bound to the same type of object. Or, is a TCB in the blocked state and is not schedulable.