diff options
Diffstat (limited to 'transfer/doc/Makefile')
| -rw-r--r-- | transfer/doc/Makefile | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/transfer/doc/Makefile b/transfer/doc/Makefile new file mode 100644 index 000000000..02f0bec10 --- /dev/null +++ b/transfer/doc/Makefile @@ -0,0 +1,41 @@ +FIGURES= + +NAME=typesystem + +default: pdf + +ps: $(NAME).ps + +pdf: $(NAME).pdf + +%.ps: %.dvi + dvips -f $^ > $@ + +#%.pdf: %.ps +# ps2pdf $^ + +%.pdf: %.dvi + dvipdfm $^ + +%.dvi: %.tex # %.bib + latex $* +# bibtex $* +# latex $* +# latex $* + +%.ps: %.dot + dot -Tps -o $@ $^ + +%.eps: %.ps + ps2epsi $^ $@ + +$(NAME).dvi: $(FIGURES) + +clean: + -rm -f *.aux *.dvi *.log *.blg *.bbl *.toc + +psclean: clean + -rm -f *.pdf *.ps + +show: $(NAME).dvi + xdvi $(NAME).dvi |