Mercurial > cpdt > repo
changeset 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 | 524458532b76 |
| children | d9e1fb184672 |
| files | Makefile |
| diffstat | 1 files changed, 2 insertions(+), 2 deletions(-) [+] |
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/