Remove file no longer needed.
authorBen Pfaff <blp@cs.stanford.edu>
Thu, 17 Mar 2005 18:21:14 +0000 (18:21 +0000)
committerBen Pfaff <blp@cs.stanford.edu>
Thu, 17 Mar 2005 18:21:14 +0000 (18:21 +0000)
grading/filesys/patches/00panic.patch [deleted file]

diff --git a/grading/filesys/patches/00panic.patch b/grading/filesys/patches/00panic.patch
deleted file mode 100644 (file)
index b7d68f0..0000000
+++ /dev/null
@@ -1,23 +0,0 @@
-This patch forces debug_panic() to terminate Bochs.
-It is in upstream now, so it is probably time to remove it.
-
-diff -up pintos/src/lib/debug.c~ pintos/src/lib/debug.c
---- pintos/src/lib/debug.c~    2004-09-12 13:14:11.000000000 -0700
-+++ pintos/src/lib/debug.c     2004-10-17 00:02:32.000000000 -0700
-@@ -5,6 +5,7 @@
- #include <stdio.h>
- #include <string.h>
- #ifdef KERNEL
-+#include "threads/init.h"
- #include "threads/interrupt.h"
- #include "devices/serial.h"
- #else
-@@ -83,7 +84,7 @@ debug_panic (const char *file, int line,
- #ifdef KERNEL
-   serial_flush ();
--  for (;;);
-+  power_off ();
- #else
-   exit (1);
- #endif