diff Makefile @ 210:b149a07b9b5b

Most old Sestoft suggestions processed
author Adam Chlipala <adamc@hcoop.net>
date Mon, 09 Nov 2009 13:18:46 -0500
parents b9e9ff52913c
children 3227be370687
line wrap: on
line diff
--- a/Makefile	Mon Nov 09 11:48:27 2009 -0500
+++ b/Makefile	Mon Nov 09 13:18:46 2009 -0500
@@ -41,9 +41,9 @@
 	coqdoc --interpolate --latex -s $< -o $@
 
 latex/%.dvi: latex/%.tex
-	latex $< ; latex $<
+	cd latex ; latex $* ; latex $*
 
-latex/%.pdf: latex/%.dvi
+%.pdf: %.dvi
 	pdflatex $<
 
 html: Makefile $(VS) src/toc.html