# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1350926934 14400
# Node ID 39c204d2262c6e038ab47222668d84db4e74f6ce
# Parent  524458532b761f8866145e74b84386b4e5ab615c
Remove hyperlinks to standard library, which were broken anyway

diff -r 524458532b76 -r 39c204d2262c Makefile
--- a/Makefile	Sun Oct 14 11:50:28 2012 -0400
+++ b/Makefile	Mon Oct 22 13:28:54 2012 -0400
@@ -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 \
+	cd src ; coqdoc --interpolate --latex --body-only -s --no-externals \
 		$*.v -o ../latex/$*.v.tex
 
 latex/cpdt.pdf: latex/cpdt.tex $(TEX) latex/cpdt.bib
@@ -40,7 +40,7 @@
 
 html: Makefile $(VS) src/toc.html
 	mkdir -p html
-	cd src ; coqdoc --interpolate $(VS_DOC) \
+	cd src ; coqdoc --interpolate --no-externals $(VS_DOC) \
 		-d ../html
 	cp src/toc.html html/