diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-20 08:41:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-20 08:41:08 +0000 |
| commit | af84fd0ae6fae303885b2026a17c2b62e7d84f18 (patch) | |
| tree | 8cfd37c96f826c45a923c910d01b9e3066a9534d /doc/Makefile.doc | |
| parent | eb97b03781c4f76ff5fb0e1efadcdb6d94f1b653 (diff) | |
Don't make link to index.html
Diffstat (limited to 'doc/Makefile.doc')
| -rw-r--r-- | doc/Makefile.doc | 1 |
1 files changed, 0 insertions, 1 deletions
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 |