diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-06-19 12:09:50 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-06-19 12:09:50 +0000 |
| commit | 818c480807ec414ed6fd1f20be4ae155d0784d9c (patch) | |
| tree | 224f2b577049987bc05b887c88a3430de42a0f13 /doc/Makefile.doc | |
| parent | 7739af043c30ac4360bb9b139562605d20cc4be6 (diff) | |
Account for new default behaviour of texi2html, using subdir for manuals
Diffstat (limited to 'doc/Makefile.doc')
| -rw-r--r-- | doc/Makefile.doc | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Makefile.doc b/doc/Makefile.doc index 94ab1d05..7b2e9ccd 100644 --- a/doc/Makefile.doc +++ b/doc/Makefile.doc @@ -126,8 +126,8 @@ dvi: ProofGeneralPortrait.eps $(DOCNAME).dvi ps: dvi $(DOCNAME).ps psz: ps $(DOCNAME).ps.gz pdf: ProofGeneralPortrait.pdf $(DOCNAME).pdf -html: $(DOCNAME).html - ln -sf $(DOCNAME)_toc.html index.html +html: $(DOCNAME)/$(DOCNAME).html + ln -sf $(DOCNAME)/$(DOCNAME)_toc.html index.html info: ProofGeneral.txt $(DOCNAME).info # NB: for info, could make localdir automatically from |