diff Makefile @ 320:21229271f44c

Fix 'make clean'
author Adam Chlipala <adam@chlipala.net>
date Mon, 12 Sep 2011 18:57:05 -0400
parents d5787b70cf48
children 06d11a6363cd
line wrap: on
line diff
--- a/Makefile	Mon Sep 12 16:47:43 2011 -0400
+++ b/Makefile	Mon Sep 12 18:57:05 2011 -0400
@@ -24,7 +24,7 @@
 clean:: Makefile.coq
 	$(MAKE) -f Makefile.coq clean
 	rm -f Makefile.coq .depend cpdt.tgz templates/*.v
-	cd latex; rm -f *.sty *.log *.aux *.dvi *.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out
+	cd latex; rm -f *.sty *.log *.aux *.dvi *.v.tex *.toc *.bbl *.blg *.idx *.ilg *.pdf *.ind *.out
 
 doc: latex/cpdt.pdf html