diff options
| author | Felipe Boeira <felipe.boeira@liu.se> | 2019-01-08 18:39:03 +0100 |
|---|---|---|
| committer | Felipe Boeira <felipe.boeira@liu.se> | 2019-01-08 18:39:03 +0100 |
| commit | d4522b8e9854178473adcea0fbb84f23f6e744bd (patch) | |
| tree | fbcf620617c5023154eba3f965b3a982daa64a47 /src/Makefile.kernel | |
| download | pintos-d4522b8e9854178473adcea0fbb84f23f6e744bd.tar.gz | |
Initial commit
Diffstat (limited to 'src/Makefile.kernel')
| -rw-r--r-- | src/Makefile.kernel | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Makefile.kernel b/src/Makefile.kernel new file mode 100644 index 0000000..162a411 --- /dev/null +++ b/src/Makefile.kernel @@ -0,0 +1,20 @@ +# -*- 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 |