aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authornotin2008-04-29 12:33:12 +0000
committernotin2008-04-29 12:33:12 +0000
commit2ead6184bda0292926dc84834003798a2ae47c19 (patch)
treeb156422f4f0c77382440ba1ca42f94a20428d255 /Makefile.build
parent73798a12d39b03e1823b93c1364a86d14e2eec0a (diff)
Correction d'un bug dans coq_makefile: génération des règles implicites en présence de l'option -custom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index bf5cdc5ada..1a8b90e2fe 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -542,7 +542,7 @@ $(GALLINA): $(GALLINACMO)
$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ config/coq_config.cmo tools/coq_makefile.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
$(COQTEX): tools/coq-tex.cmo
$(SHOW)'OCAMLC -o $@'