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