added debug configuration option for decoding framework

[palacios.git] / palacios / src / palacios / vmm_v3dec.c

diff --git a/palacios/src/palacios/vmm_v3dec.c b/palacios/src/palacios/vmm_v3dec.c
index 74c8c56..c1df822 100644 (file)
--- a/palacios/src/palacios/vmm_v3dec.c
+++ b/palacios/src/palacios/vmm_v3dec.c
@@ -20,6 +20,11 @@
 #include <palacios/vmm_decoder.h>
 #include <palacios/vmm_instr_decoder.h>
 
+#ifndef CONFIG_DEBUG_DECODER
+#undef PrintDebug
+#define PrintDebug(fmt, args...)
+#endif
+
 
 #define MASK(val, length) ({                                           \
             ullong_t mask = 0x0LL;                                     \