diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-25 13:04:51 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-25 13:04:51 +0000 |
| commit | 0702539ad300891ca5590aa552d893fe1561505c (patch) | |
| tree | 7022b0b5117b70f8dbb7091f5033b0ca80ee70dc /doc/Makefile | |
| parent | 0d3c430f178c9cc9867a349d535a4a53dea551c2 (diff) | |
Replaced ProofGeneral.texi with NewDoc.texi. Deleted NewDoc.texi
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/Makefile b/doc/Makefile index fa3020fa..7401acfe 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -67,20 +67,21 @@ info: $(DOCNAME).info clean: rm -f $(DOCNAME).?? $(DOCNAME).fns $(DOCNAME).vrs $(DOCNAME).cps rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc $(DOCNAME).cp0 + rm -f $(DOCNAME).kys rm -f *~ ## ## distclean: Remove documentation targets ## distclean: clean - rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME).pdf $(DOCNAME)*.html + rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME)*.ps $(DOCNAME).pdf $(DOCNAME)*.html ## -## magic: update magic comments in NewDoc.texi from docstrings in code. +## texi: update magic comments in texi from docstrings in code. ## (developer use only!) ## -magic: - $(EMACS) -l docstring-magic.el NewDoc.texi -f texi-docstring-magic -f save-buffer +$(DOCNAME).texi: ../*/*.el + $(EMACS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer |