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.


build fixes to merge the Palacios configuration parameters with Linux parameters.
[palacios.git] / palacios / include / palacios / vmm_time.h
index c9248b8..329fce6 100644 (file)
@@ -92,7 +92,7 @@ static inline uint64_t v3_get_host_time(struct vm_time *t) {
 
 // Returns *monotonic* guest time.
 static inline uint64_t v3_get_guest_time(struct vm_time *t) {
-#ifdef CONFIG_TIME_HIDE_VM_COST
+#ifdef V3_CONFIG_TIME_HIDE_VM_COST
     V3_ASSERT(t->exit_time);
     return t->exit_time + t->guest_host_offset;
 #else