--- Gnu-Mach/ddb/db_output.h	2020/09/02 04:45:48	1.1.1.3
+++ Gnu-Mach/ddb/db_output.h	2020/09/02 04:48:18	1.1.1.4
@@ -32,9 +32,15 @@
  * Printing routines for kernel debugger.
  */
 
+#ifndef _DDB_DB_OUTPUT_H_
+#define _DDB_DB_OUTPUT_H_
+
 extern void	db_force_whitespace(void);
-extern int	db_print_position(void);
+extern int	db_print_position(void) __attribute__ ((pure));
 extern void	db_end_line(void);
 extern void	db_printf(const char *fmt, ...);
+/* alternate name */
+#define kdbprintf db_printf
 extern void	db_putchar(int c);
-extern void	kdbprintf(const char *fmt, ...);
+
+#endif /* _DDB_DB_OUTPUT_H_ */