aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authornotin2006-03-08 10:47:12 +0000
committernotin2006-03-08 10:47:12 +0000
commit5dc8776314d30fd045f3092bea4056642ff121e8 (patch)
tree125583cc2e8aaa8144e3f957089f1e3b7edafb9e /Makefile
parentf8776bb49cf701d687405ea627c660b62941fea7 (diff)
r8620@thot: notin | 2006-03-08 11:44:16 +0100
Modifications diverses de Coqdoc: - modification du comportement par défaut de l'option --latex - ajout d'une option --stdout - réaménagement dans les sources (création de global.ml) - modification du parser de coqdoc pour regler les problèmes liés à  la syntaxe V8. - Correction du bug #1052 sur les commentaires en fin de ligne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8617 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile6
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index c7e91cd5ae..97122d438c 100644
--- a/Makefile
+++ b/Makefile
@@ -1115,9 +1115,9 @@ $(COQWC): tools/coqwc.cmo
beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml
-COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \
- tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \
- tools/coqdoc/main.cmo
+COQDOCCMO=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
+ tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
+ tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
$(COQDOC): $(COQDOCCMO)
$(SHOW)'OCAMLC -o $@'