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.


Fixed major palacios barrier implementation error with potentially serious implicatio...
[palacios.git] / Kconfig
diff --git a/Kconfig b/Kconfig
index bcf3ef7..5edd454 100644 (file)
--- a/Kconfig
+++ b/Kconfig
@@ -357,6 +357,13 @@ config DEBUG_TIME
        help
          This turns on debugging of system time virtualization
 
+config DEBUG_SCHEDULER
+    bool "Scheduler"
+    default n
+    depends on DEBUG_ON
+    help
+      This turns on debugging for scheduler
+
 config DEBUG_IO
        bool "IO"
        default n
@@ -387,6 +394,13 @@ config DEBUG_HALT
        help 
          This turns on debugging for the halt instruction handler
 
+config DEBUG_MWAIT
+       bool "MWAIT/MONITOR"
+       default n
+       depends on DEBUG_ON
+       help 
+         This turns on debugging for the mwait and monitor instruction handlers
+
 config DEBUG_DEV_MGR
        bool "Device Manager"
        default n