diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-09-24 15:43:19 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-09-24 15:43:19 +0000 |
| commit | 06ebdec620f8c2daa4a59660b0a9f2bce7eea5de (patch) | |
| tree | 2ee13546dfa8aca62820ee63c935862629d00014 /doc/Makefile | |
| parent | 2a59e48560620133eac3899f4c12ca81e4a4d55e (diff) | |
Removed Makefiles from distribution.
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/doc/Makefile b/doc/Makefile index 2799d5ac..bf262c5e 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -15,13 +15,9 @@ DOCNAME = ProofGeneral -# program to make info files from .texi MAKEINFO = makeinfo -# program to make dvi files from .texi TEXI2DVI = texi2dvi -# program to make pdf files from .texi TEXI2PDF = texi2pdf -# program to make html files from .texi TEXI2HTML = texi2html .SUFFIXES: .texi .info .dvi .html .pdf @@ -63,8 +59,8 @@ info: $(DOCNAME).info ## clean: Remove subsidiary documentation files ## clean: - rm -f $(DOCNAME).?? $(DOCNAME).cps $(DOCNAME).cp0 - rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc + rm -f $(DOCNAME).?? $(DOCNAME).fns $(DOCNAME).vrs $(DOCNAME).cps + rm -f $(DOCNAME).aux $(DOCNAME).log $(DOCNAME).toc $(DOCNAME).cp0 rm -f *~ ## @@ -74,11 +70,6 @@ distclean: clean rm -f $(DOCNAME).info* $(DOCNAME).dvi $(DOCNAME).pdf $(DOCNAME)*.html -## -## cvsclean: remove all non-cvs -## -cvsclean: distclean - |