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.


Check to make sure extension name is provided
authorKyle Hale <kh@u.northwestern.edu>
Thu, 5 Jul 2012 19:32:37 +0000 (14:32 -0500)
committerPeter Dinda <pdinda@northwestern.edu>
Sat, 7 Jul 2012 22:30:44 +0000 (17:30 -0500)
commit38d4628c6eb960164ae8d7c6fffe3820b9d6acb9
tree8f9564230553ac3a575b36c2403b80f349cdb944
parentb7093fd3602ef2c796a1f8a0daded9d6aad0b756
Check to make sure extension name is provided

Fixes a null pointer dereference that occurs if an extension is
provided without a name
palacios/src/palacios/vmm_config.c