X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=Makefile;h=acdb23d2f94672f4d7b02b8babc34e7df9bd7029;hb=2847b62110d877f18a65bbbb91d406e064fefff2;hp=f6cd61bd9716efbec3c3611a68a17cba39be7b6a;hpb=b3141dc15538accd8566de0d1e39b3f2f02650cb;p=pspp

diff --git a/Makefile b/Makefile
index f6cd61bd97..acdb23d2f9 100644
--- a/Makefile
+++ b/Makefile
@@ -9,14 +9,8 @@
 all:
 
 # Produce the documentation in readable form.
-info:
-	cd doc && $(MAKE) info
-html:
-	cd doc && $(MAKE) html
-dvi:
-	cd doc && $(MAKE) dvi && $(MAKE) mostlyclean
-pdf:
-	cd doc && $(MAKE) pdf && $(MAKE) mostlyclean
+info html dvi pdf:
+	cd doc && $(MAKE) $@ && $(MAKE) mostlyclean
 
 # Perform some platform independent checks on the gnulib code.
 check: