Still working on timer updates, heading towards being able to have a CPU

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

diff --git a/palacios/src/palacios/vmx_handler.c b/palacios/src/palacios/vmx_handler.c
index 9d29f9f..357f0d2 100644 (file)
--- a/palacios/src/palacios/vmx_handler.c
+++ b/palacios/src/palacios/vmx_handler.c
@@ -100,15 +100,16 @@ int v3_handle_vmx_exit(struct guest_info * info, struct vmx_exit_info * exit_inf
 
             break;
 
-#if 0
         case VMEXIT_RDTSC:
+#ifdef CONFIG_DEBUG_TIME
+           PrintDebug("RDTSC\n");
+#endif 
            if (v3_handle_rdtsc(info) == -1) {
                PrintError("Error Handling RDTSC instruction\n");
                return -1;
            }
            
            break;
-#endif
 
         case VMEXIT_CPUID:
            if (v3_handle_cpuid(info) == -1) {