1 files changed, 1 insertions, 4 deletions
diff --git a/kern/machine.c b/kern/machine.c
index 871801e0..97181a84 100644
--- a/kern/machine.c
+++ b/kern/machine.c
@@ -51,6 +51,7 @@
 #include <kern/task.h>
 #include <kern/thread.h>
 #include <machine/machspl.h>	/* for splsched */
+#include <machine/model_dep.h>
 #include <sys/reboot.h>
 
 
@@ -688,10 +689,6 @@ Restart_pset:
  */
 
 #ifdef __GNUC__
-extern __volatile__ void halt_cpu();
-#endif
-
-#ifdef __GNUC__
 __volatile__
 #endif
 void processor_doshutdown(processor)