diff Makefile @ 503:929c12a95b87

Add back in external LaTeX links
author Adam Chlipala <adam@chlipala.net>
date Sat, 09 Feb 2013 10:15:53 -0500
parents a95af5a59990
children 136d4b84eb96
line wrap: on
line diff
--- a/Makefile	Tue Feb 05 17:05:09 2013 -0500
+++ b/Makefile	Sat Feb 09 10:15:53 2013 -0500
@@ -29,7 +29,7 @@
 doc: latex/cpdt.pdf html
 
 latex/%.v.tex: Makefile src/%.v src/%.glob
-	cd src ; coqdoc --interpolate --latex --body-only -s --no-externals \
+	cd src ; coqdoc --interpolate --latex --body-only -s \
 		$*.v -o ../latex/$*.v.tex
 
 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib