int debug_puts(const char *);
debug_puts writes the string s to the Debug Terminal followed by a new-line character.
debug_puts returns -1 if a write error occurs, otherwise it returns a nonnegative value.