Add support for a pdf version of the user manual

diff --git a/Makefile b/Makefile
index 51581973ab1c75e847474948bbe444db261b0e53..b1456a2e5b93d13f0883d3280fc3509ecd6aa638 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1306,6 +1306,9 @@ html:
 info:
        $(MAKE) -C Documentation info
 
+pdf:
+       $(MAKE) -C Documentation pdf
+
 TAGS:
        $(RM) TAGS
        $(FIND) . -name '*.[hcS]' -print | xargs etags -a
@@ -1448,6 +1451,9 @@ install-html:
 install-info:
        $(MAKE) -C Documentation install-info
 
+install-pdf:
+       $(MAKE) -C Documentation install-pdf
+
 quick-install-doc:
        $(MAKE) -C Documentation quick-install