X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=src%2Fdevices%2Fshutdown.h;h=7bcef19e7759509c7625920785bb1ef1829b22d9;hp=0bc5657b4b8716978827bc513ef9aead9bc1e97e;hb=9a4067dc5bd3d810ce4b1d9dd8ba394dee4c247b;hpb=53641f9bb07aa127b2b5e402e28b7421ce8a7f3b

diff --git a/src/devices/shutdown.h b/src/devices/shutdown.h
index 0bc5657..7bcef19 100644
--- a/src/devices/shutdown.h
+++ b/src/devices/shutdown.h
@@ -1,7 +1,9 @@
 #ifndef DEVICES_SHUTDOWN_H
 #define DEVICES_SHUTDOWN_H
 
-void shutdown_reboot (void);
-void shutdown_power_off (void);
+#include <debug.h>
+
+void shutdown_reboot (void) NO_RETURN;
+void shutdown_power_off (void) NO_RETURN;
 
 #endif /* devices/shutdown.h */