From 519114c247e82a67c2203c4bde802510ce9c40b5 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 1 Jul 1999 18:44:54 +0000 Subject: Put info files back in dist. --- doc/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/Makefile') 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 -- cgit v1.2.3