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.


added global module registry
[palacios.git] / palacios / src / palacios / vmm.c
index cf0d4bd..66ce9c0 100644 (file)
@@ -83,7 +83,12 @@ void Init_V3(struct v3_os_hooks * hooks, int num_cpus) {
     // Register all shadow paging handlers
     V3_init_shdw_paging();
 
-#ifdef INSTRUMENT_VMM
+
+#ifdef CONFIG_SYMMOD
+    V3_init_symmod();
+#endif
+
+#ifdef CONFIG_INSTRUMENT_VMM
     v3_init_instrumentation();
 #endif