- * Debug output goes to stderr in hosted applications. Freestanding (AKA embedded)
- * applications use drv/kdebug.c to output diagnostic messages to a serial terminal
- * or a JTAG debugger.
+ * Debug output goes to stderr in hosted applications.
+ * Freestanding (AKA embedded) applications use \c drv/kdebug.c to output
+ * diagnostic messages to a serial terminal or a JTAG debugger.