diff options
| -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 |