Mercurial > cpdt > repo
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/