X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=palacios%2Finclude%2Fpalacios%2Fvmm.h;h=ae4421c2e89b8c9054b41ac245a27a55cd714ba8;hb=25e188e5eb5f6e0368b206b79b9f275d050367d9;hp=9ee2bf898581af07acf1d15912dfda4d0df2cb5b;hpb=f762b666f3ea508a49b16429e185eb458aa83329;p=palacios-OLD.git

diff --git a/palacios/include/palacios/vmm.h b/palacios/include/palacios/vmm.h
index 9ee2bf8..ae4421c 100644
--- a/palacios/include/palacios/vmm.h
+++ b/palacios/include/palacios/vmm.h
@@ -22,13 +22,13 @@
 
 
 /*#include <palacios/vm_guest.h>*/
-#include <palacios/vmm_mem.h>
-#include <palacios/vmm_types.h>
 
 struct guest_info;
 
 
 #ifdef __V3VEE__
+#include <palacios/vmm_mem.h>
+#include <palacios/vmm_types.h>
 
 //#include <palacios/vmm_types.h>
 #include <palacios/vmm_string.h>
@@ -250,7 +250,9 @@ void v3_yield_cond(struct guest_info * info);
 void v3_print_cond(const char * fmt, ...);
 
 
+#ifdef CONFIG_MULTITHREAD_OS
 void v3_interrupt_cpu(struct v3_vm_info * vm, int logical_cpu, int vector);
+#endif
 
 
 v3_cpu_arch_t v3_get_cpu_type(int cpu_id);