90a91,94
>
> // Most recently used page table entries
> PTE *PTECache[2];
> inline void flushCache() { memset(PTECache, 0, 2 * sizeof(PTE*)); }