Call serial_flush() in power_off().
authorBen Pfaff <blp@cs.stanford.edu>
Tue, 21 Sep 2004 05:55:18 +0000 (05:55 +0000)
committerBen Pfaff <blp@cs.stanford.edu>
Tue, 21 Sep 2004 05:55:18 +0000 (05:55 +0000)
src/threads/init.c

index 0d9c69984603eaaa6a69bf4fac58c4af9e54ce54..26b9345879c1848ce1d7321ea6e68160854e022f 100644 (file)
@@ -278,6 +278,8 @@ power_off (void)
 #endif
 
   printf ("Powering off...\n");
+  serial_flush ();
+
   for (p = s; *p != '\0'; p++)
     outb (0x8900, *p);
   for (;;);