added 64bit support to makefiles

[palacios.git] / build / Makefile

diff --git a/build/Makefile b/build/Makefile
index 1cfd87d..e9f4435 100644 (file)
--- a/build/Makefile
+++ b/build/Makefile
@@ -195,11 +195,13 @@ palacios:
 palacios-full:
        (cd $(PALACIOS_BUILD_DIR) && make $(DEBUG_SECTIONS) world)
 
+palacios-full64:
+       (cd $(PALACIOS_BUILD_DIR) && make ARCH=64 $(DEBUG_SECTIONS) world)`     
 
 palacios-lean:
        (cd $(PALACIOS_BUILD_DIR) && make LEAN_AND_MEAN=1 world)
 
-kitten: palacios-full
+kitten: palacios-full64
        cp $(PALACIOS_BUILD_DIR)/libv3vee.a $(KITTEN_TOP_DIR)/palacios/
        cp $(PALACIOS_BUILD_DIR)/../lib/xed/libxed32e.a $(KITTEN_TOP_DIR)/palacios/
        cp $(PALACIOS_BUILD_DIR)/vm_kernel $(KITTEN_TOP_DIR)/palacios/