diff Makefile @ 473:39c204d2262c

Remove hyperlinks to standard library, which were broken anyway
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 13:28:54 -0400
parents e2c88317611f
children a95af5a59990
line wrap: on
line diff
--- 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/