Fixed (hopefully) bug introduced previously by moving update_timers outside of the...

[palacios.git] / palacios / src / devices / Kconfig

diff --git a/palacios/src/devices/Kconfig b/palacios/src/devices/Kconfig
index 456d717..685b245 100644 (file)
--- a/palacios/src/devices/Kconfig
+++ b/palacios/src/devices/Kconfig
@@ -265,6 +265,11 @@ config FILEDISK
        help
          Includes the file based disk backend
 
+config DEBUG_FILEDISK
+       bool "FILEDISK backend debugging"
+       depends on FILEDISK && DEBUG_ON
+       help 
+         Enable debugging for the file based disk backend      
 
 config NETDISK
        bool "NETDISK storage backend"
@@ -280,6 +285,11 @@ config RAMDISK
        help 
          Includes the RAM based disk backend
 
+config DEBUG_RAMDISK
+       bool "RAMDISK baskend debugging"
+       depends on RAMDISK && DEBUG_ON
+       help 
+         Enable debugging for the ram based disk backend       
 
 config TMPDISK
        bool "TMPDISK storage backend"
@@ -337,11 +347,11 @@ config SERIAL_UART
        help 
          Include virtual serial port
 
-config STREAM
-       bool "Stream device"
+config CHAR_STREAM
+       bool "Stream based character frontend"
        default n
        help
-         Stream Device
+         Include Stream based character device frontend
 
 endmenu