Skip to content

C
cpdt
Commit 7632c895 authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Remove hyperlinks to standard library, which were broken anyway

parent df735505
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
Makefile
View file @ 7632c895
......@@ -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 \
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 @@ latex/%.pdf: latex/%.tex latex/cpdt.bib
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/
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment