portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

manual: Correct VCPU_SetEPTRoot invocation parameter name

Browse source 
Changes the parameter name to match the actual object that should be passed, as required
by the kernel code.
This commit is contained in:
Adrian Danis 2017-09-07 16:13:28 +10:00
parent d3c9f36d94
commit a1a6390d65
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
libsel4/arch_include/x86/interfaces/sel4arch.xml
View file

@ -369,7 +369,7 @@
</interface>
<interface name="seL4_TCB" manual_name="TCB">
<method id="TCBSetEPTRoot" name="SetEPTRoot" condition="defined(CONFIG_VTX)" manual_name="Set EPT Root">
<param dir="in" name="vcpu" type="seL4_CPtr"/>
<param dir="in" name="eptpml4" type="seL4_CPtr"/>
</method>
</interface>
<interface name="seL4_X86_VCPU" manual_name="VCPU">