diff 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
line wrap: on
line diff
--- a/Makefile	Fri Nov 06 10:52:43 2009 -0500
+++ b/Makefile	Fri Nov 06 12:15:05 2009 -0500
@@ -43,6 +43,7 @@
 	cd latex ; pdflatex cpdt
 
 html: Makefile $(VS) src/toc.html
+	mkdir -p html
 	cd src ; coqdoc $(VS_DOC) \
 		--glob-from ../$(GLOBALS) \
 		-d ../html