T243: Fix vnode_objsize() to return 1024 for ARM_l2 vnodes

Signed-off-by: Simon Gerber <simon.gerber@inf.ethz.ch>

diff --git a/include/barrelfish_kpi/capabilities.h b/include/barrelfish_kpi/capabilities.h
index 3ab6002..8b687bf 100644 (file)
--- a/include/barrelfish_kpi/capabilities.h
+++ b/include/barrelfish_kpi/capabilities.h
@@ -177,9 +177,7 @@ static inline size_t vnode_objsize(enum objtype type)
     }
     else if (type == ObjType_VNode_ARM_l2)
     {
-        // XXX: should be 1024, once we get around to untangling the ARMv7
-        // page table mess, cf. T243.
-        return 4096;
+        return 1024;
     }
 
     assert(0 && !"Page table size unknown.");