From af84fd0ae6fae303885b2026a17c2b62e7d84f18 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 20 Aug 2009 08:41:08 +0000 Subject: Don't make link to index.html --- doc/Makefile.doc | 1 - 1 file changed, 1 deletion(-) (limited to 'doc/Makefile.doc') diff --git a/doc/Makefile.doc b/doc/Makefile.doc index f952c9c0..f1830915 100644 --- a/doc/Makefile.doc +++ b/doc/Makefile.doc @@ -128,7 +128,6 @@ psz: ps $(DOCNAME).ps.gz pdf: ProofGeneralPortrait.pdf $(DOCNAME).pdf # da: target is a fake: we actually make in a subdir html: $(DOCNAME).html - ln -sf $(DOCNAME)/$(DOCNAME)_toc.html index.html info: ProofGeneral.txt $(DOCNAME).info # NB: for info, could make localdir automatically from -- cgit v1.2.3