diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-06-28 17:42:03 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-06-28 17:42:03 +0000 |
| commit | 0823923dded755c26f868a6846a89cd0da4d2356 (patch) | |
| tree | 2c2bf51b475d246e8a6522d1f2bcfddaab64b4f4 /doc/Makefile | |
| parent | 9a422e337c054f3498c3ddd1fdf141baea606705 (diff) | |
Removed accidental deletion of ps file.
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/doc/Makefile b/doc/Makefile index c46965ec..e53fd339 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -75,9 +75,9 @@ ProofGeneral.eps: doc: dvi info ## -## all : build dvi, ps, html, info +## all : build all documentation targets ## -all: dvi ps html info +all: dvi ps html info dvi: ProofGeneral.eps $(DOCNAME).dvi ps: $(DOCNAME).ps @@ -94,9 +94,8 @@ info: ProofGeneral.txt $(DOCNAME).info ## clean: rm -f ProofGeneral.txt ProofGeneral.eps - 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 $(DOCNAME).{cp,fn,vr,tp,ky,pg} + rm -f $(DOCNAME).{fns,vrs,cps,aux,log,toc,kys,cp0} rm -f *~ ## |