TCB API: Fix minor discrepancy: seL4_CNode was used for VSpace roots

This commit is contained in:
Kofi Doku Atuah 2018-11-06 10:40:17 +11:00
parent f1f6f975b6
commit a96e005924

View file

@ -129,7 +129,7 @@
description="The new CSpace root."/>
<param dir="in" name="cspace_root_data" type="seL4_Word"
description="Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect."/>
<param dir="in" name="vspace_root" type="seL4_CNode"
<param dir="in" name="vspace_root" type="seL4_CPtr"
description="The new VSpace root."/>
<param dir="in" name="vspace_root_data" type="seL4_Word"
description="Has no effect on x86 or ARM processors."/>
@ -206,7 +206,7 @@
description="The new CSpace root."/>
<param dir="in" name="cspace_root_data" type="seL4_Word"
description="Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect."/>
<param dir="in" name="vspace_root" type="seL4_CNode"
<param dir="in" name="vspace_root" type="seL4_CPtr"
description="The new VSpace root."/>
<param dir="in" name="vspace_root_data" type="seL4_Word"
description="Has no effect on x86 or ARM processors."/>