Palacios Public Git Repository

To checkout Palacios execute

  git clone http://v3vee.org/palacios/palacios.web/palacios.git
This will give you the master branch. You probably want the devel branch or one of the release branches. To switch to the devel branch, simply execute
  cd palacios
  git checkout --track -b devel origin/devel
The other branches are similar.


cleaned up instrumentation implementation
[palacios.git] / palacios / build / Makefile
index 8fbe2a2..0f98a56 100644 (file)
@@ -219,8 +219,14 @@ endif
 
 ifeq ($(INSTRUMENT_VMM),1)
   EXTRA_C_OPTS:= -DINSTRUMENT_VMM
+  INSTRUMENT_OPT := -finstrument-functions
+  OBJ_FILES := palacios/vmm_instrument.o
+else
+  INSTRUMENT_OPT := 
 endif
 
+
+
 # ----------------------------------------------------------------------
 # Configuration -
 #   Various options specifying how GeekOS should be built,
@@ -273,7 +279,7 @@ VMM_OBJS := \
        palacios/vmm_profiler.o \
        palacios/vmm_direct_paging.o \
        palacios/vmm_ringbuffer.o \
-       palacios/vmm_instrument.o \
+       $(OBJ_FILES)
 
 #              vmx.c vmcs_gen.c vmcs.c
 
@@ -407,11 +413,6 @@ CC_GENERAL_OPTS = \
 #-fPIC \
 #-fvisibility=hidden
 
-ifeq ($(INSTRUMENT_VMM),1)
-       INSTRUMENT_OPT = -finstrument-functions
-else
-       INSTRUMENT_OPT = 
-endif
 
 # Flags passed to objcopy program (strip unnecessary sections from kernel.exe)
 OBJCOPY_FLAGS := -R .dynamic -R .note -R .comment