From: Ben Pfaff Date: Thu, 17 Mar 2005 18:21:14 +0000 (+0000) Subject: Remove file no longer needed. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d5859f34033fee47c7ae626ea2d3c0b5d83cfe3b;p=pintos-anon Remove file no longer needed. --- diff --git a/grading/filesys/patches/00panic.patch b/grading/filesys/patches/00panic.patch deleted file mode 100644 index b7d68f0..0000000 --- a/grading/filesys/patches/00panic.patch +++ /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 - #include - #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