Arm32: Fix vcpu_hw_write_reg
Forgotten in commit 5bce5c0c1e.
Signed-off-by: Indan Zupancic <indan@nul.nu>
This commit is contained in:
parent
4172bd6170
commit
b527b46dec
1 changed files with 0 additions and 2 deletions
|
|
@ -619,11 +619,9 @@ static void vcpu_hw_write_reg(word_t reg_index, word_t reg)
|
|||
case seL4_VCPUReg_CNTVOFFlow:
|
||||
set_cntv_off_low(reg);
|
||||
break;
|
||||
#ifdef ENABLE_SMP_SUPPORT
|
||||
case seL4_VCPUReg_VMPIDR:
|
||||
set_vmpidr(reg);
|
||||
break;
|
||||
#endif /* ENABLE_SMP_SUPPORT */
|
||||
default:
|
||||
fail("ARM/HYP: Invalid register index");
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue