--- Gnu-Mach/ddb/db_output.h	2020/09/02 04:36:57	1.1
+++ Gnu-Mach/ddb/db_output.h	2020/09/02 04:52:35	1.1.1.5
@@ -32,13 +32,15 @@
  * Printing routines for kernel debugger.
  */
 
-extern void	db_force_whitespace();
-extern int	db_print_position();
-extern void	db_end_line();
-#if 1
-extern void	db_printf();
-#else
-extern void	db_printf( char *fmt, ...);
-#endif
+#ifndef _DDB_DB_OUTPUT_H_
+#define _DDB_DB_OUTPUT_H_
 
+extern void	db_force_whitespace(void);
+extern int	db_print_position(void) __attribute__ ((pure));
+extern void	db_end_line(void);
+extern int	db_printf(const char *fmt, ...);
+/* alternate name */
+#define kdbprintf db_printf
+extern void	db_putchar(int c);
 
+#endif /* _DDB_DB_OUTPUT_H_ */