changeset 503:929c12a95b87

Add back in external LaTeX links
author Adam Chlipala <adam@chlipala.net>
date Sat, 09 Feb 2013 10:15:53 -0500
parents 7d2339cbd39c
children 04177dd1b133
files Makefile
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
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