doc-src/TutorialI/Makefile
changeset 12676 99e7b2045d8f
parent 12672 f85386e8acdf
child 12677 73c070d5c031
equal deleted inserted replaced
12675:25f1e89b5012 12676:99e7b2045d8f
    27 	isabelle.sty isabellesym.sty ../pdfsetup.sty
    27 	isabelle.sty isabellesym.sty ../pdfsetup.sty
    28 
    28 
    29 dvi: $(NAME).dvi
    29 dvi: $(NAME).dvi
    30 
    30 
    31 $(NAME).dvi: $(FILES) isabelle_hol.eps Types/typedef.eps
    31 $(NAME).dvi: $(FILES) isabelle_hol.eps Types/typedef.eps
    32 	@ln -sf Types/typedef.eps .
    32 	@test -r typedef.eps || ln -s ../gfx/typedef.ps .
    33 	$(LATEX) $(NAME)
    33 	$(LATEX) $(NAME)
    34 	$(BIBTEX) $(NAME)
    34 	$(BIBTEX) $(NAME)
    35 	$(LATEX) $(NAME)
    35 	$(LATEX) $(NAME)
    36 	$(LATEX) $(NAME)
    36 	$(LATEX) $(NAME)
    37 	$(SEDINDEX) $(NAME)
    37 	$(SEDINDEX) $(NAME)
    38 	$(LATEX) $(NAME)
    38 	$(LATEX) $(NAME)
    39 
    39 
    40 pdf: $(NAME).pdf
    40 pdf: $(NAME).pdf
    41 
    41 
    42 $(NAME).pdf: $(FILES) isabelle_hol.pdf Types/typedef.pdf
    42 $(NAME).pdf: $(FILES) isabelle_hol.pdf Types/typedef.pdf
    43 	@ln -sf Types/typedef.pdf .
    43 	@test -r typedef.pdf || ln -s ../gfx/typedef.pdf .
    44 	$(PDFLATEX) $(NAME)
    44 	$(PDFLATEX) $(NAME)
    45 	$(BIBTEX) $(NAME)
    45 	$(BIBTEX) $(NAME)
    46 	$(PDFLATEX) $(NAME)
    46 	$(PDFLATEX) $(NAME)
    47 	$(PDFLATEX) $(NAME)
    47 	$(PDFLATEX) $(NAME)
    48 	$(SEDINDEX) $(NAME)
    48 	$(SEDINDEX) $(NAME)