Add back in external LaTeX links

d22609d4 · Adam Chlipala · 14076b2b · d22609d4
Commit d22609d4 authored Feb 09, 2013 by Adam Chlipala
Show whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

Makefile Makefile +1 -1

No files found.
--- a/Makefile
+++ b/Makefile
@@ -29,7 +29,7 @@ clean:: Makefile.coq
 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