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