/* Print an integer as hex digits. 
This function will put the hex digits of a 32-bit integer into the print buffer. It does not add the '0x'-prefix. */
void dbg_print_hexint(uint32_t out_int)
/* Print an integer as hex digits. 
This function will put the hex digits of a 32-bit integer into the print buffer. It does not add the '0x'-prefix. */
void dbg_print_hexint(uint32_t out_int)
{
	char out_str[2 * sizeof(out_int)];
	dbg_sprint_hexint(out_str, out_int);
	_dbg_wait_for_lock();
	_dbg_putstr(out_str, sizeof(out_str));
	_dbg_unlock();
}