comparison Makefile @ 473:39c204d2262c

Remove hyperlinks to standard library, which were broken anyway
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 13:28:54 -0400
parents e2c88317611f
children a95af5a59990
comparison
equal deleted inserted replaced
472:524458532b76 473:39c204d2262c
27 cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out 27 cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out
28 28
29 doc: latex/cpdt.pdf html 29 doc: latex/cpdt.pdf html
30 30
31 latex/%.v.tex: Makefile src/%.v src/%.glob 31 latex/%.v.tex: Makefile src/%.v src/%.glob
32 cd src ; coqdoc --interpolate --latex --body-only -s \ 32 cd src ; coqdoc --interpolate --latex --body-only -s --no-externals \
33 $*.v -o ../latex/$*.v.tex 33 $*.v -o ../latex/$*.v.tex
34 34
35 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib 35 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib
36 cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt 36 cd latex ; pdflatex cpdt ; pdflatex cpdt ; bibtex cpdt ; makeindex cpdt ; pdflatex cpdt ; pdflatex cpdt
37 37
38 latex/%.pdf: latex/%.tex latex/cpdt.bib 38 latex/%.pdf: latex/%.tex latex/cpdt.bib
39 cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $* 39 cd latex ; pdflatex $* ; pdflatex $* ; bibtex $* ; makeindex $* ; pdflatex $* ; pdflatex $*
40 40
41 html: Makefile $(VS) src/toc.html 41 html: Makefile $(VS) src/toc.html
42 mkdir -p html 42 mkdir -p html
43 cd src ; coqdoc --interpolate $(VS_DOC) \ 43 cd src ; coqdoc --interpolate --no-externals $(VS_DOC) \
44 -d ../html 44 -d ../html
45 cp src/toc.html html/ 45 cp src/toc.html html/
46 46
47 templates: $(TEMPLATES) 47 templates: $(TEMPLATES)
48 48