diff options
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 0000000..a3ecaf2 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,20 @@ +GENERATED_EPS_IMAGES = $(addsuffix .eps,$(basename $(shell echo bilder/*.dia))) +GENERATED_PDF_IMAGES = $(addsuffix .pdf,$(basename $(GENERATED_EPS_IMAGES))) + +build: $(GENERATED_PDF_IMAGES) + pdflatex pvs-doc + pdflatex pvs-doc + makeindex pvs-doc + pdflatex pvs-doc +.PHONY: build + +clean: + rm -f $(GENERATED_PDF_IMAGES) $(GENERATED_EPS_IMAGES) + rm -f pvs-doc.aux pvs-doc.idx pvs-doc.ilg pvs-doc.ing pvs-doc.log pvs-doc.out pvs-doc.pdf pvs-doc.toc +.PHONY: clean + +%.eps : %.dia + dia -e $@ $< + +%.pdf : %.eps + epstopdf --outfile=$@ $< |