*** empty log message ***

[palacios.git] / palacios / src / geekos / vmm_stubs.c

diff --git a/palacios/src/geekos/vmm_stubs.c b/palacios/src/geekos/vmm_stubs.c
index 96145db..a9db9c6 100644 (file)
--- a/palacios/src/geekos/vmm_stubs.c
+++ b/palacios/src/geekos/vmm_stubs.c
@@ -2,6 +2,9 @@
 #include <geekos/serial.h>
 
 
+
+void * Identity(void *addr) { return addr; };
+
 void * Allocate_VMM_Pages(int num_pages) {
   void * start_page = Alloc_Page();
   SerialPrint("Allocating Page: %x (%d of %d)\n",start_page, 1, num_pages);