From: Ben Pfaff <blp@cs.stanford.edu>
Date: Tue, 21 Sep 2004 05:55:18 +0000 (+0000)
Subject: Call serial_flush() in power_off().
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=9dda658ddc5ada7718cbb6855ad8b0b64ed92ec6;p=pintos-anon

Call serial_flush() in power_off().
---

diff --git a/src/threads/init.c b/src/threads/init.c
index 0d9c699..26b9345 100644
--- a/src/threads/init.c
+++ b/src/threads/init.c
@@ -278,6 +278,8 @@ power_off (void)
 #endif
 
   printf ("Powering off...\n");
+  serial_flush ();
+
   for (p = s; *p != '\0'; p++)
     outb (0x8900, *p);
   for (;;);