1 // Some platforms (Linux) don't define PAGESIZE, set a default value in that 2 // case. 3 #include <limits.h> 4 5 #ifndef PAGESIZE 6 #define PAGESIZE 4096 7 #endif 8 9 #include <../os/kernel/OS.h> 10