update

[l4.git] / l4 / pkg / libvcpu / include / vcpu.h

diff --git a/l4/pkg/libvcpu/include/vcpu.h b/l4/pkg/libvcpu/include/vcpu.h
index 751051fd4ec535b5f3373163d18a819bea41f6dc..3e014a591ce5cf1c9ea99498eec7e4a888e8a069 100644 (file)
--- a/l4/pkg/libvcpu/include/vcpu.h
+++ b/l4/pkg/libvcpu/include/vcpu.h
@@ -296,6 +296,8 @@ l4vcpu_irq_restore(l4_vcpu_state_t *vcpu, l4vcpu_irq_state_t s,
 {
   if (s & L4_VCPU_F_IRQ)
     l4vcpu_irq_enable(vcpu, utcb, do_event_work_cb, setup_ipc);
+  else if (vcpu->state & L4_VCPU_F_IRQ)
+    l4vcpu_irq_disable(vcpu);
 }
 
 L4_CV L4_INLINE