comparison Makefile @ 205:f05514cc6c0d

'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents cbf2f74a5130
children 3f4576f15130
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
41 41
42 latex/cpdt.pdf: latex/cpdt.dvi 42 latex/cpdt.pdf: latex/cpdt.dvi
43 cd latex ; pdflatex cpdt 43 cd latex ; pdflatex cpdt
44 44
45 html: Makefile $(VS) src/toc.html 45 html: Makefile $(VS) src/toc.html
46 mkdir -p html
46 cd src ; coqdoc $(VS_DOC) \ 47 cd src ; coqdoc $(VS_DOC) \
47 --glob-from ../$(GLOBALS) \ 48 --glob-from ../$(GLOBALS) \
48 -d ../html 49 -d ../html
49 cp src/toc.html html/ 50 cp src/toc.html html/
50 51