if ((r=sendrec(m->m_source, &st)) != OK) {
printf("DEV_STATUS failed to %d: %d\n", m->m_source, r);
if (r == EDEADSRCDST) return;
+ if (r == EDSTDIED) return;
+ if (r == ESRCDIED) return;
panic(__FILE__,"couldn't sendrec for DEV_STATUS", r);
}
for (;;) {
if (r != OK) {
if (r == EDEADSRCDST) return; /* give up */
+ if (r == EDSTDIED) return;
+ if (r == ESRCDIED) return;
else panic(__FILE__,"call_task: can't send/receive", r);
}