From: Ben Pfaff Date: Sun, 31 Oct 2004 06:29:22 +0000 (+0000) Subject: Add -*- makefile -*- line. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=041ca90618ae20ee141b030cac1381f4c1504d58;p=pintos-anon Add -*- makefile -*- line. --- diff --git a/src/Makefile.kernel b/src/Makefile.kernel index fe63d52..181eb23 100644 --- a/src/Makefile.kernel +++ b/src/Makefile.kernel @@ -1,3 +1,5 @@ +# -*- makefile -*- + include Make.vars BUILD_SUBDIRS = $(addprefix build/, $(SUBDIRS)) CP = cp