+void stdio_print_current_devices(void)
+{
+#ifndef CONFIG_SYS_CONSOLE_INFO_QUIET
+ /* Print information */
+ puts("In: ");
+ if (stdio_devices[stdin] == NULL) {
+ puts("No input devices available!\n");
+ } else {
+ printf ("%s\n", stdio_devices[stdin]->name);
+ }
+
+ puts("Out: ");
+ if (stdio_devices[stdout] == NULL) {
+ puts("No output devices available!\n");
+ } else {
+ printf ("%s\n", stdio_devices[stdout]->name);
+ }
+
+ puts("Err: ");
+ if (stdio_devices[stderr] == NULL) {
+ puts("No error devices available!\n");
+ } else {
+ printf ("%s\n", stdio_devices[stderr]->name);
+ }
+#endif /* CONFIG_SYS_CONSOLE_INFO_QUIET */
+}
+