X-Git-Url: http://v3vee.org/palacios/gitweb/gitweb.cgi?a=blobdiff_plain;f=build%2FMakefile;h=012e2f8995d14becdbf1992ad78a24b6a26cd3e2;hb=bbef87558ec784cd99c72b759aa78a8c47aa5fd3;hp=a217d7daee61f7b56a58c5e112609b0f0577b52e;hpb=746934f539c53c6fc687890c02ebf886c6873342;p=palacios.git

diff --git a/build/Makefile b/build/Makefile
index a217d7d..012e2f8 100644
--- a/build/Makefile
+++ b/build/Makefile
@@ -160,6 +160,9 @@ ifeq ($(PROFILE_VMM),1)
   GEEKOS_FLAGS:= $(GEEKOS_FLAGS) PROFILE_VMM=1
 endif
 
+ifeq ($(INSTRUMENT_VMM),1)
+  GEEKOS_FLAGS:= $(GEEKOS_FLAGS) INSTRUMENT_VMM=1
+endif
 
 # ----------------------------------------------------------------------
 # Targets -