1 files changed, 4 insertions, 1 deletions
diff --git a/src/include/kernel/pagemgr.H b/src/include/kernel/pagemgr.H
index 5c22d6864..52d924b79 100644
--- a/src/include/kernel/pagemgr.H
+++ b/src/include/kernel/pagemgr.H
@@ -32,7 +32,10 @@ class PageManager
     private:
 	void* _allocatePage(size_t);
 	void _freePage(void*, size_t);
-	
+
+            /** Statistics on number of free pages (for debug) */
+        uint64_t iv_pagesAvail;
+
 	struct page_t
 	{
 	    page_t* next;