1 files changed, 0 insertions, 20 deletions

diff --git a/pintos-progos/Makefile.kernel b/pintos-progos/Makefile.kernel
deleted file mode 100644
index 162a411..0000000
--- a/pintos-progos/Makefile.kernel
+++ /dev/null
@@ -1,20 +0,0 @@
-# -*- makefile -*-
-
-all:
-
-include Make.vars
-
-DIRS = $(sort $(addprefix build/,$(KERNEL_SUBDIRS) $(TEST_SUBDIRS) lib/user))
-
-all grade check: $(DIRS) build/Makefile
-        cd build && $(MAKE) $@
-$(DIRS):
-        mkdir -p $@
-build/Makefile: ../Makefile.build
-        cp $< $@
-
-build/%: $(DIRS) build/Makefile
-        cd build && $(MAKE) $*
-
-clean:
-        rm -rf build