summaryrefslogtreecommitdiff
path: root/Makefile.doc
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc
index 795e0e5c..f481d681 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -209,7 +209,7 @@ else
doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
endif
$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
- -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
(cd doc/stdlib;\