--- Gnu-Mach/ddb/db_input.h	2020/09/02 04:45:48	1.1
+++ Gnu-Mach/ddb/db_input.h	2020/09/02 04:48:18	1.1.1.2
@@ -25,4 +25,6 @@
 
 extern int db_readline (char *lstart, int lsize);
 
+extern void db_check_interrupt(void);
+
 #endif /* _DDB_DB_INPUT_H_ */