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.


Use passed in options to set scheduler
authorPatrick G. Bridges <bridges@cs.unm.edu>
Thu, 21 Feb 2013 20:15:45 +0000 (13:15 -0700)
committerPatrick G. Bridges <bridges@cs.unm.edu>
Thu, 21 Feb 2013 20:15:45 +0000 (13:15 -0700)
commitc53e6ed4d6903df3c8351b8334848c466076d5b0
tree2477e1f9eb973172dcc672e6f8c7b5c091ea9c3d
parentc1810f8134ef829599525d30856970f0155da1f3
Use passed in options to set scheduler
palacios/src/extensions/ext_sched_edf.c
palacios/src/palacios/vmm_scheduler.c