T238: fix vnode_objsize() to not use BASE_PAGE_SIZE but 4096
authorSimon Gerber <simon.gerber@inf.ethz.ch>
Wed, 25 May 2016 10:50:20 +0000 (12:50 +0200)
committerSimon Gerber <simon.gerber@inf.ethz.ch>
Wed, 25 May 2016 10:50:21 +0000 (12:50 +0200)
commit2746d7b36b19d3be7fbcd771f87f55856ccbdd3c
tree236262e73e6a94d2dabe9077d0f68c923cfc5ab2
parent1b84fe2dc91e2d2bb7ddaae3c13d01f2dc1b34d1
T238: fix vnode_objsize() to not use BASE_PAGE_SIZE but 4096

This is necessary because asmoffsets.c includes
include/barrelfish_kpi/capabilities.h but does not include the appropriate
headers to get BASE_PAGE_SIZE and related definitions.

Signed-off-by: Simon Gerber <simon.gerber@inf.ethz.ch>
include/barrelfish_kpi/capabilities.h