From a1a6390d650632d06b403bf267dc4d2aca59d7a1 Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@data61.csiro.au>
Date: Thu, 7 Sep 2017 16:13:28 +1000
Subject: [PATCH] manual: Correct VCPU_SetEPTRoot invocation parameter name

Changes the parameter name to match the actual object that should be passed, as required
by the kernel code.
---
 libsel4/arch_include/x86/interfaces/sel4arch.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libsel4/arch_include/x86/interfaces/sel4arch.xml b/libsel4/arch_include/x86/interfaces/sel4arch.xml
index 94fd65afb..237b4d2fa 100644
--- a/libsel4/arch_include/x86/interfaces/sel4arch.xml
+++ b/libsel4/arch_include/x86/interfaces/sel4arch.xml
@@ -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">