# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1360422953 18000
# Node ID 929c12a95b87d4571c4c473539edef1ae1073e0f
# Parent  7d2339cbd39c5fc8ecff8ed071d9ea2921fe74ad
Add back in external LaTeX links

diff -r 7d2339cbd39c -r 929c12a95b87 Makefile
--- 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