diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile index 03e99ad510..09051c00ba 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -69,8 +69,8 @@ FTPHTMLDOCS=doc-html.tar.gz all: check-env all-dvi all-pdf check-env: - if $(TEST) "$(COQBIN)" = ""; then echo "COQBIN undefined"; exit 1; fi - if $(TEST) "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; fi + @if $(TEST) "$(COQBIN)" = ""; then echo "COQBIN undefined"; exit 1; fi + @if $(TEST) "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; fi coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex |