From: Ben Pfaff <blp@cs.stanford.edu>
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?p=pintos-anon;a=commitdiff_plain;h=d5859f34033fee47c7ae626ea2d3c0b5d83cfe3b

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 <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