aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--doc/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Makefile b/doc/Makefile
index d136277d..9013b8f1 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -85,7 +85,7 @@ all: dvi ps html info pdf
##
## dist: build distribution targets
##
-dist: html psz
+dist: info html psz
dvi: ProofGeneral.eps $(DOCNAME).dvi
ps: dvi $(DOCNAME).ps