X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=Makefile;h=fbc8f4ec8e372c5a224ad1698a03a625bbeeb271;hb=21848a29ff6f6d52751bd91463be03b790f6e3e5;hp=2c374e72bf33b40f32c6476d6b5013a6258910db;hpb=615bf3b3d2a8573ed6fb9ddc0055745e163ac999;p=pintos-anon

diff --git a/Makefile b/Makefile
index 2c374e7..fbc8f4e 100644
--- a/Makefile
+++ b/Makefile
@@ -10,4 +10,4 @@ distclean:: clean
 	find . -name '*~' -exec rm '{}' \;
 
 check::
-	make -C tests $@
+	$(MAKE) -C tests $@