1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% SPDX-License-Identifier: GPL-2.0-only 5% 6 7\apidoc 8{debug_putchar} 9{Debug - Put Character} 10{Print a character to the console} 11{static inline void seL4\_DebugPutChar} 12{ 13\param{char}{c}{The character to print.} 14} 15{\noret} 16{Prints a character to the serial port, if debugging is turned on.} 17