From 82f668132e5b7742943f6dc7edf680fb8fe33968 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 19 Jun 2007 12:27:06 +0000
Subject: Revert html target to not include dir (although it builds in dir)

---
 doc/Makefile.doc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/doc/Makefile.doc b/doc/Makefile.doc
index 7b2e9ccd..c6531b95 100644
--- a/doc/Makefile.doc
+++ b/doc/Makefile.doc
@@ -126,7 +126,8 @@ dvi:    ProofGeneralPortrait.eps $(DOCNAME).dvi
 ps:	dvi $(DOCNAME).ps
 psz:	ps $(DOCNAME).ps.gz
 pdf:    ProofGeneralPortrait.pdf $(DOCNAME).pdf
-html:   $(DOCNAME)/$(DOCNAME).html
+# 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
 
-- 
cgit v1.2.3