use make variable to avoid QA issue: "make[1]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule" --- a/GNUmakefile +++ b/GNUmakefile @@ -576,7 +576,7 @@ doc/home-page.html: doc/home-page.lisp # xdoc::save that populates doc/manual/ (not under books/). acl2-manual: check-books rm -rf doc/manual books/system/doc/acl2-manual.cert - cd books ; make USE_QUICKLISP=1 system/doc/acl2-manual.cert + cd books ; $(MAKE) USE_QUICKLISP=1 system/doc/acl2-manual.cert rm -rf doc/manual/download/* # WARNING: The dependency list just below isn't complete, since it