Print statistics at power off.

[pintos-anon] / src / lib / kernel / console.h

diff --git a/src/lib/kernel/console.h b/src/lib/kernel/console.h
index 6e5b41bd79473f035d57a885ee6234a0b9c3d728..788edf2309d1ce94a0c312454d51c3f811ecd634 100644 (file)
--- a/src/lib/kernel/console.h
+++ b/src/lib/kernel/console.h
@@ -2,5 +2,6 @@
 #define __LIB_KERNEL_CONSOLE_H
 
 void console_init (void);
+void console_print_stats (void);
 
 #endif /* lib/kernel/console.h */