Mercurial > cpdt > repo
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 |